1(*  Title:      HOL/HOLCF/Powerdomains.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Powerdomains\<close>
6
7theory Powerdomains
8imports ConvexPD Domain
9begin
10
11subsection \<open>Universal domain embeddings\<close>
12
13definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
14definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
15
16definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))"
17definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))"
18
19definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))"
20definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))"
21
22lemma ep_pair_upper: "ep_pair upper_emb upper_prj"
23  unfolding upper_emb_def upper_prj_def
24  by (simp add: ep_pair_udom approx_chain_upper_map)
25
26lemma ep_pair_lower: "ep_pair lower_emb lower_prj"
27  unfolding lower_emb_def lower_prj_def
28  by (simp add: ep_pair_udom approx_chain_lower_map)
29
30lemma ep_pair_convex: "ep_pair convex_emb convex_prj"
31  unfolding convex_emb_def convex_prj_def
32  by (simp add: ep_pair_udom approx_chain_convex_map)
33
34subsection \<open>Deflation combinators\<close>
35
36definition upper_defl :: "udom defl \<rightarrow> udom defl"
37  where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
38
39definition lower_defl :: "udom defl \<rightarrow> udom defl"
40  where "lower_defl = defl_fun1 lower_emb lower_prj lower_map"
41
42definition convex_defl :: "udom defl \<rightarrow> udom defl"
43  where "convex_defl = defl_fun1 convex_emb convex_prj convex_map"
44
45lemma cast_upper_defl:
46  "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj"
47using ep_pair_upper finite_deflation_upper_map
48unfolding upper_defl_def by (rule cast_defl_fun1)
49
50lemma cast_lower_defl:
51  "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj"
52using ep_pair_lower finite_deflation_lower_map
53unfolding lower_defl_def by (rule cast_defl_fun1)
54
55lemma cast_convex_defl:
56  "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj"
57using ep_pair_convex finite_deflation_convex_map
58unfolding convex_defl_def by (rule cast_defl_fun1)
59
60subsection \<open>Domain class instances\<close>
61
62instantiation upper_pd :: ("domain") "domain"
63begin
64
65definition
66  "emb = upper_emb oo upper_map\<cdot>emb"
67
68definition
69  "prj = upper_map\<cdot>prj oo upper_prj"
70
71definition
72  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
73
74definition
75  "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
76
77definition
78  "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
79
80definition
81  "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
82
83instance proof
84  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
85    unfolding emb_upper_pd_def prj_upper_pd_def
86    by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
87next
88  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
89    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
90    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
91qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+
92
93end
94
95instantiation lower_pd :: ("domain") "domain"
96begin
97
98definition
99  "emb = lower_emb oo lower_map\<cdot>emb"
100
101definition
102  "prj = lower_map\<cdot>prj oo lower_prj"
103
104definition
105  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
106
107definition
108  "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
109
110definition
111  "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
112
113definition
114  "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
115
116instance proof
117  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
118    unfolding emb_lower_pd_def prj_lower_pd_def
119    by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
120next
121  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
122    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
123    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
124qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+
125
126end
127
128instantiation convex_pd :: ("domain") "domain"
129begin
130
131definition
132  "emb = convex_emb oo convex_map\<cdot>emb"
133
134definition
135  "prj = convex_map\<cdot>prj oo convex_prj"
136
137definition
138  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
139
140definition
141  "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
142
143definition
144  "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
145
146definition
147  "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
148
149instance proof
150  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
151    unfolding emb_convex_pd_def prj_convex_pd_def
152    by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
153next
154  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
155    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
156    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
157qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+
158
159end
160
161lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
162by (rule defl_upper_pd_def)
163
164lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
165by (rule defl_lower_pd_def)
166
167lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
168by (rule defl_convex_pd_def)
169
170subsection \<open>Isomorphic deflations\<close>
171
172lemma isodefl_upper:
173  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
174apply (rule isodeflI)
175apply (simp add: cast_upper_defl cast_isodefl)
176apply (simp add: emb_upper_pd_def prj_upper_pd_def)
177apply (simp add: upper_map_map)
178done
179
180lemma isodefl_lower:
181  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
182apply (rule isodeflI)
183apply (simp add: cast_lower_defl cast_isodefl)
184apply (simp add: emb_lower_pd_def prj_lower_pd_def)
185apply (simp add: lower_map_map)
186done
187
188lemma isodefl_convex:
189  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
190apply (rule isodeflI)
191apply (simp add: cast_convex_defl cast_isodefl)
192apply (simp add: emb_convex_pd_def prj_convex_pd_def)
193apply (simp add: convex_map_map)
194done
195
196subsection \<open>Domain package setup for powerdomains\<close>
197
198lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
199lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
200lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
201
202lemmas [domain_deflation] =
203  deflation_upper_map deflation_lower_map deflation_convex_map
204
205setup \<open>
206  fold Domain_Take_Proofs.add_rec_type
207    [(\<^type_name>\<open>upper_pd\<close>, [true]),
208     (\<^type_name>\<open>lower_pd\<close>, [true]),
209     (\<^type_name>\<open>convex_pd\<close>, [true])]
210\<close>
211
212end
213