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