|
1 (* Title: HOLCF/Domain.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Domain package *} |
|
6 |
|
7 theory Domain |
|
8 imports Bifinite Domain_Aux |
|
9 uses |
|
10 ("Tools/domaindef.ML") |
|
11 ("Tools/Domain/domain_isomorphism.ML") |
|
12 ("Tools/Domain/domain_axioms.ML") |
|
13 ("Tools/Domain/domain.ML") |
|
14 begin |
|
15 |
|
16 default_sort "domain" |
|
17 |
|
18 subsection {* Representations of types *} |
|
19 |
|
20 lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x" |
|
21 by (simp add: cast_DEFL) |
|
22 |
|
23 lemma emb_prj_emb: |
|
24 fixes x :: "'a" |
|
25 assumes "DEFL('a) \<sqsubseteq> DEFL('b)" |
|
26 shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x" |
|
27 unfolding emb_prj |
|
28 apply (rule cast.belowD) |
|
29 apply (rule monofun_cfun_arg [OF assms]) |
|
30 apply (simp add: cast_DEFL) |
|
31 done |
|
32 |
|
33 lemma prj_emb_prj: |
|
34 assumes "DEFL('a) \<sqsubseteq> DEFL('b)" |
|
35 shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)" |
|
36 apply (rule emb_eq_iff [THEN iffD1]) |
|
37 apply (simp only: emb_prj) |
|
38 apply (rule deflation_below_comp1) |
|
39 apply (rule deflation_cast) |
|
40 apply (rule deflation_cast) |
|
41 apply (rule monofun_cfun_arg [OF assms]) |
|
42 done |
|
43 |
|
44 text {* Isomorphism lemmas used internally by the domain package: *} |
|
45 |
|
46 lemma domain_abs_iso: |
|
47 fixes abs and rep |
|
48 assumes DEFL: "DEFL('b) = DEFL('a)" |
|
49 assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb" |
|
50 assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb" |
|
51 shows "rep\<cdot>(abs\<cdot>x) = x" |
|
52 unfolding abs_def rep_def |
|
53 by (simp add: emb_prj_emb DEFL) |
|
54 |
|
55 lemma domain_rep_iso: |
|
56 fixes abs and rep |
|
57 assumes DEFL: "DEFL('b) = DEFL('a)" |
|
58 assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb" |
|
59 assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb" |
|
60 shows "abs\<cdot>(rep\<cdot>x) = x" |
|
61 unfolding abs_def rep_def |
|
62 by (simp add: emb_prj_emb DEFL) |
|
63 |
|
64 subsection {* Deflations as sets *} |
|
65 |
|
66 definition defl_set :: "defl \<Rightarrow> udom set" |
|
67 where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}" |
|
68 |
|
69 lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)" |
|
70 unfolding defl_set_def by simp |
|
71 |
|
72 lemma defl_set_bottom: "\<bottom> \<in> defl_set A" |
|
73 unfolding defl_set_def by simp |
|
74 |
|
75 lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A" |
|
76 unfolding defl_set_def by simp |
|
77 |
|
78 lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B" |
|
79 apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric]) |
|
80 apply (auto simp add: cast.belowI cast.belowD) |
|
81 done |
|
82 |
|
83 subsection {* Proving a subtype is representable *} |
|
84 |
|
85 text {* Temporarily relax type constraints. *} |
|
86 |
|
87 setup {* |
|
88 fold Sign.add_const_constraint |
|
89 [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) |
|
90 , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) |
|
91 , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) |
|
92 , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) |
|
93 , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"}) |
|
94 , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ] |
|
95 *} |
|
96 |
|
97 lemma typedef_liftdomain_class: |
|
98 fixes Rep :: "'a::pcpo \<Rightarrow> udom" |
|
99 fixes Abs :: "udom \<Rightarrow> 'a::pcpo" |
|
100 fixes t :: defl |
|
101 assumes type: "type_definition Rep Abs (defl_set t)" |
|
102 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
103 assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" |
|
104 assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" |
|
105 assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)" |
|
106 assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" |
|
107 assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" |
|
108 assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))" |
|
109 shows "OFCLASS('a, liftdomain_class)" |
|
110 using liftemb [THEN meta_eq_to_obj_eq] |
|
111 using liftprj [THEN meta_eq_to_obj_eq] |
|
112 proof (rule liftdomain_class_intro) |
|
113 have emb_beta: "\<And>x. emb\<cdot>x = Rep x" |
|
114 unfolding emb |
|
115 apply (rule beta_cfun) |
|
116 apply (rule typedef_cont_Rep [OF type below adm_defl_set]) |
|
117 done |
|
118 have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)" |
|
119 unfolding prj |
|
120 apply (rule beta_cfun) |
|
121 apply (rule typedef_cont_Abs [OF type below adm_defl_set]) |
|
122 apply simp_all |
|
123 done |
|
124 have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x" |
|
125 using type_definition.Rep [OF type] |
|
126 unfolding prj_beta emb_beta defl_set_def |
|
127 by (simp add: type_definition.Rep_inverse [OF type]) |
|
128 have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y" |
|
129 unfolding prj_beta emb_beta |
|
130 by (simp add: type_definition.Abs_inverse [OF type]) |
|
131 show "ep_pair (emb :: 'a \<rightarrow> udom) prj" |
|
132 apply default |
|
133 apply (simp add: prj_emb) |
|
134 apply (simp add: emb_prj cast.below) |
|
135 done |
|
136 show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)" |
|
137 by (rule cfun_eqI, simp add: defl emb_prj) |
|
138 show "LIFTDEFL('a) = u_defl\<cdot>DEFL('a)" |
|
139 unfolding liftdefl .. |
|
140 qed |
|
141 |
|
142 lemma typedef_DEFL: |
|
143 assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)" |
|
144 shows "DEFL('a::pcpo) = t" |
|
145 unfolding assms .. |
|
146 |
|
147 text {* Restore original typing constraints. *} |
|
148 |
|
149 setup {* |
|
150 fold Sign.add_const_constraint |
|
151 [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"}) |
|
152 , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"}) |
|
153 , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"}) |
|
154 , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"}) |
|
155 , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"}) |
|
156 , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ] |
|
157 *} |
|
158 |
|
159 use "Tools/domaindef.ML" |
|
160 |
|
161 subsection {* Isomorphic deflations *} |
|
162 |
|
163 definition |
|
164 isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool" |
|
165 where |
|
166 "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj" |
|
167 |
|
168 lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t" |
|
169 unfolding isodefl_def by (simp add: cfun_eqI) |
|
170 |
|
171 lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))" |
|
172 unfolding isodefl_def by (simp add: cfun_eqI) |
|
173 |
|
174 lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>" |
|
175 unfolding isodefl_def |
|
176 by (drule cfun_fun_cong [where x="\<bottom>"], simp) |
|
177 |
|
178 lemma isodefl_imp_deflation: |
|
179 fixes d :: "'a \<rightarrow> 'a" |
|
180 assumes "isodefl d t" shows "deflation d" |
|
181 proof |
|
182 note assms [unfolded isodefl_def, simp] |
|
183 fix x :: 'a |
|
184 show "d\<cdot>(d\<cdot>x) = d\<cdot>x" |
|
185 using cast.idem [of t "emb\<cdot>x"] by simp |
|
186 show "d\<cdot>x \<sqsubseteq> x" |
|
187 using cast.below [of t "emb\<cdot>x"] by simp |
|
188 qed |
|
189 |
|
190 lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)" |
|
191 unfolding isodefl_def by (simp add: cast_DEFL) |
|
192 |
|
193 lemma isodefl_LIFTDEFL: |
|
194 "isodefl (u_map\<cdot>(ID :: 'a \<rightarrow> 'a)) LIFTDEFL('a::predomain)" |
|
195 unfolding u_map_ID DEFL_u [symmetric] |
|
196 by (rule isodefl_ID_DEFL) |
|
197 |
|
198 lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID" |
|
199 unfolding isodefl_def |
|
200 apply (simp add: cast_DEFL) |
|
201 apply (simp add: cfun_eq_iff) |
|
202 apply (rule allI) |
|
203 apply (drule_tac x="emb\<cdot>x" in spec) |
|
204 apply simp |
|
205 done |
|
206 |
|
207 lemma isodefl_bottom: "isodefl \<bottom> \<bottom>" |
|
208 unfolding isodefl_def by (simp add: cfun_eq_iff) |
|
209 |
|
210 lemma adm_isodefl: |
|
211 "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))" |
|
212 unfolding isodefl_def by simp |
|
213 |
|
214 lemma isodefl_lub: |
|
215 assumes "chain d" and "chain t" |
|
216 assumes "\<And>i. isodefl (d i) (t i)" |
|
217 shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)" |
|
218 using prems unfolding isodefl_def |
|
219 by (simp add: contlub_cfun_arg contlub_cfun_fun) |
|
220 |
|
221 lemma isodefl_fix: |
|
222 assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)" |
|
223 shows "isodefl (fix\<cdot>f) (fix\<cdot>g)" |
|
224 unfolding fix_def2 |
|
225 apply (rule isodefl_lub, simp, simp) |
|
226 apply (induct_tac i) |
|
227 apply (simp add: isodefl_bottom) |
|
228 apply (simp add: assms) |
|
229 done |
|
230 |
|
231 lemma isodefl_abs_rep: |
|
232 fixes abs and rep and d |
|
233 assumes DEFL: "DEFL('b) = DEFL('a)" |
|
234 assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb" |
|
235 assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb" |
|
236 shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t" |
|
237 unfolding isodefl_def |
|
238 by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb) |
|
239 |
|
240 lemma isodefl_sfun: |
|
241 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
242 isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)" |
|
243 apply (rule isodeflI) |
|
244 apply (simp add: cast_sfun_defl cast_isodefl) |
|
245 apply (simp add: emb_sfun_def prj_sfun_def) |
|
246 apply (simp add: sfun_map_map isodefl_strict) |
|
247 done |
|
248 |
|
249 lemma isodefl_ssum: |
|
250 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
251 isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)" |
|
252 apply (rule isodeflI) |
|
253 apply (simp add: cast_ssum_defl cast_isodefl) |
|
254 apply (simp add: emb_ssum_def prj_ssum_def) |
|
255 apply (simp add: ssum_map_map isodefl_strict) |
|
256 done |
|
257 |
|
258 lemma isodefl_sprod: |
|
259 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
260 isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)" |
|
261 apply (rule isodeflI) |
|
262 apply (simp add: cast_sprod_defl cast_isodefl) |
|
263 apply (simp add: emb_sprod_def prj_sprod_def) |
|
264 apply (simp add: sprod_map_map isodefl_strict) |
|
265 done |
|
266 |
|
267 lemma isodefl_cprod: |
|
268 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
269 isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)" |
|
270 apply (rule isodeflI) |
|
271 apply (simp add: cast_prod_defl cast_isodefl) |
|
272 apply (simp add: emb_prod_def prj_prod_def) |
|
273 apply (simp add: cprod_map_map cfcomp1) |
|
274 done |
|
275 |
|
276 lemma isodefl_u: |
|
277 fixes d :: "'a::liftdomain \<rightarrow> 'a" |
|
278 shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)" |
|
279 apply (rule isodeflI) |
|
280 apply (simp add: cast_u_defl cast_isodefl) |
|
281 apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq) |
|
282 apply (simp add: u_map_map) |
|
283 done |
|
284 |
|
285 lemma encode_prod_u_map: |
|
286 "encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x)) |
|
287 = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x" |
|
288 unfolding encode_prod_u_def decode_prod_u_def |
|
289 apply (case_tac x, simp, rename_tac a b) |
|
290 apply (case_tac a, simp, case_tac b, simp, simp) |
|
291 done |
|
292 |
|
293 lemma isodefl_cprod_u: |
|
294 assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl (u_map\<cdot>d2) t2" |
|
295 shows "isodefl (u_map\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (sprod_defl\<cdot>t1\<cdot>t2)" |
|
296 using assms unfolding isodefl_def |
|
297 apply (simp add: emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def) |
|
298 apply (simp add: emb_u_def [symmetric] prj_u_def [symmetric]) |
|
299 apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map) |
|
300 done |
|
301 |
|
302 lemma encode_cfun_map: |
|
303 "encode_cfun\<cdot>(cfun_map\<cdot>f\<cdot>g\<cdot>(decode_cfun\<cdot>x)) |
|
304 = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x" |
|
305 unfolding encode_cfun_def decode_cfun_def |
|
306 apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def) |
|
307 apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all) |
|
308 done |
|
309 |
|
310 lemma isodefl_cfun: |
|
311 "isodefl (u_map\<cdot>d1) t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
312 isodefl (cfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)" |
|
313 apply (rule isodeflI) |
|
314 apply (simp add: cast_sfun_defl cast_isodefl) |
|
315 apply (simp add: emb_cfun_def prj_cfun_def encode_cfun_map) |
|
316 apply (simp add: sfun_map_map isodefl_strict) |
|
317 done |
|
318 |
|
319 subsection {* Setting up the domain package *} |
|
320 |
|
321 use "Tools/Domain/domain_isomorphism.ML" |
|
322 use "Tools/Domain/domain_axioms.ML" |
|
323 use "Tools/Domain/domain.ML" |
|
324 |
|
325 setup Domain_Isomorphism.setup |
|
326 |
|
327 lemmas [domain_defl_simps] = |
|
328 DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u |
|
329 liftdefl_eq LIFTDEFL_prod |
|
330 |
|
331 lemmas [domain_map_ID] = |
|
332 cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID |
|
333 |
|
334 lemmas [domain_isodefl] = |
|
335 isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod |
|
336 isodefl_cfun isodefl_cprod isodefl_cprod_u |
|
337 |
|
338 lemmas [domain_deflation] = |
|
339 deflation_cfun_map deflation_sfun_map deflation_ssum_map |
|
340 deflation_sprod_map deflation_cprod_map deflation_u_map |
|
341 |
|
342 setup {* |
|
343 fold Domain_Take_Proofs.add_rec_type |
|
344 [(@{type_name cfun}, [true, true]), |
|
345 (@{type_name "sfun"}, [true, true]), |
|
346 (@{type_name ssum}, [true, true]), |
|
347 (@{type_name sprod}, [true, true]), |
|
348 (@{type_name prod}, [true, true]), |
|
349 (@{type_name "u"}, [true])] |
|
350 *} |
|
351 |
|
352 end |