1 (* Title: HOL/HOLCF/Powerdomains.thy |
1 (* Title: HOL/HOLCF/Powerdomains.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Powerdomains *} |
5 section \<open>Powerdomains\<close> |
6 |
6 |
7 theory Powerdomains |
7 theory Powerdomains |
8 imports ConvexPD Domain |
8 imports ConvexPD Domain |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Universal domain embeddings *} |
11 subsection \<open>Universal domain embeddings\<close> |
12 |
12 |
13 definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
13 definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
14 definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
14 definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
15 |
15 |
16 definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))" |
16 definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))" |
29 |
29 |
30 lemma ep_pair_convex: "ep_pair convex_emb convex_prj" |
30 lemma ep_pair_convex: "ep_pair convex_emb convex_prj" |
31 unfolding convex_emb_def convex_prj_def |
31 unfolding convex_emb_def convex_prj_def |
32 by (simp add: ep_pair_udom approx_chain_convex_map) |
32 by (simp add: ep_pair_udom approx_chain_convex_map) |
33 |
33 |
34 subsection {* Deflation combinators *} |
34 subsection \<open>Deflation combinators\<close> |
35 |
35 |
36 definition upper_defl :: "udom defl \<rightarrow> udom defl" |
36 definition upper_defl :: "udom defl \<rightarrow> udom defl" |
37 where "upper_defl = defl_fun1 upper_emb upper_prj upper_map" |
37 where "upper_defl = defl_fun1 upper_emb upper_prj upper_map" |
38 |
38 |
39 definition lower_defl :: "udom defl \<rightarrow> udom defl" |
39 definition lower_defl :: "udom defl \<rightarrow> udom defl" |
55 lemma cast_convex_defl: |
55 lemma cast_convex_defl: |
56 "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj" |
56 "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj" |
57 using ep_pair_convex finite_deflation_convex_map |
57 using ep_pair_convex finite_deflation_convex_map |
58 unfolding convex_defl_def by (rule cast_defl_fun1) |
58 unfolding convex_defl_def by (rule cast_defl_fun1) |
59 |
59 |
60 subsection {* Domain class instances *} |
60 subsection \<open>Domain class instances\<close> |
61 |
61 |
62 instantiation upper_pd :: ("domain") "domain" |
62 instantiation upper_pd :: ("domain") "domain" |
63 begin |
63 begin |
64 |
64 |
65 definition |
65 definition |
165 by (rule defl_lower_pd_def) |
165 by (rule defl_lower_pd_def) |
166 |
166 |
167 lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)" |
167 lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)" |
168 by (rule defl_convex_pd_def) |
168 by (rule defl_convex_pd_def) |
169 |
169 |
170 subsection {* Isomorphic deflations *} |
170 subsection \<open>Isomorphic deflations\<close> |
171 |
171 |
172 lemma isodefl_upper: |
172 lemma isodefl_upper: |
173 "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" |
173 "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" |
174 apply (rule isodeflI) |
174 apply (rule isodeflI) |
175 apply (simp add: cast_upper_defl cast_isodefl) |
175 apply (simp add: cast_upper_defl cast_isodefl) |
191 apply (simp add: cast_convex_defl cast_isodefl) |
191 apply (simp add: cast_convex_defl cast_isodefl) |
192 apply (simp add: emb_convex_pd_def prj_convex_pd_def) |
192 apply (simp add: emb_convex_pd_def prj_convex_pd_def) |
193 apply (simp add: convex_map_map) |
193 apply (simp add: convex_map_map) |
194 done |
194 done |
195 |
195 |
196 subsection {* Domain package setup for powerdomains *} |
196 subsection \<open>Domain package setup for powerdomains\<close> |
197 |
197 |
198 lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex |
198 lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex |
199 lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID |
199 lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID |
200 lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex |
200 lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex |
201 |
201 |
202 lemmas [domain_deflation] = |
202 lemmas [domain_deflation] = |
203 deflation_upper_map deflation_lower_map deflation_convex_map |
203 deflation_upper_map deflation_lower_map deflation_convex_map |
204 |
204 |
205 setup {* |
205 setup \<open> |
206 fold Domain_Take_Proofs.add_rec_type |
206 fold Domain_Take_Proofs.add_rec_type |
207 [(@{type_name "upper_pd"}, [true]), |
207 [(@{type_name "upper_pd"}, [true]), |
208 (@{type_name "lower_pd"}, [true]), |
208 (@{type_name "lower_pd"}, [true]), |
209 (@{type_name "convex_pd"}, [true])] |
209 (@{type_name "convex_pd"}, [true])] |
210 *} |
210 \<close> |
211 |
211 |
212 end |
212 end |