1 (* Title: HOLCF/Library/Strict_Fun.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* The Strict Function Type *} |
|
6 |
|
7 theory Strict_Fun |
|
8 imports HOLCF |
|
9 begin |
|
10 |
|
11 pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) |
|
12 = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}" |
|
13 by simp_all |
|
14 |
|
15 type_notation (xsymbols) |
|
16 sfun (infixr "\<rightarrow>!" 0) |
|
17 |
|
18 text {* TODO: Define nice syntax for abstraction, application. *} |
|
19 |
|
20 definition |
|
21 sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)" |
|
22 where |
|
23 "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))" |
|
24 |
|
25 definition |
|
26 sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b" |
|
27 where |
|
28 "sfun_rep = (\<Lambda> f. Rep_sfun f)" |
|
29 |
|
30 lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f" |
|
31 unfolding sfun_rep_def by (simp add: cont_Rep_sfun) |
|
32 |
|
33 lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>" |
|
34 unfolding sfun_rep_beta by (rule Rep_sfun_strict) |
|
35 |
|
36 lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>" |
|
37 unfolding sfun_rep_beta by (rule Rep_sfun [simplified]) |
|
38 |
|
39 lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f" |
|
40 by (simp add: cfun_eq_iff strictify_conv_if) |
|
41 |
|
42 lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f" |
|
43 unfolding sfun_abs_def sfun_rep_def |
|
44 apply (simp add: cont_Abs_sfun cont_Rep_sfun) |
|
45 apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse) |
|
46 apply (simp add: cfun_eq_iff strictify_conv_if) |
|
47 apply (simp add: Rep_sfun [simplified]) |
|
48 done |
|
49 |
|
50 lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f" |
|
51 unfolding sfun_abs_def sfun_rep_def |
|
52 apply (simp add: cont_Abs_sfun cont_Rep_sfun) |
|
53 apply (simp add: Abs_sfun_inverse) |
|
54 done |
|
55 |
|
56 lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs" |
|
57 apply default |
|
58 apply (rule sfun_abs_sfun_rep) |
|
59 apply (simp add: cfun_below_iff strictify_conv_if) |
|
60 done |
|
61 |
|
62 interpretation sfun: ep_pair sfun_rep sfun_abs |
|
63 by (rule ep_pair_sfun) |
|
64 |
|
65 subsection {* Map functional for strict function space *} |
|
66 |
|
67 definition |
|
68 sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)" |
|
69 where |
|
70 "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)" |
|
71 |
|
72 lemma sfun_map_ID [domain_map_ID]: "sfun_map\<cdot>ID\<cdot>ID = ID" |
|
73 unfolding sfun_map_def |
|
74 by (simp add: cfun_map_ID cfun_eq_iff) |
|
75 |
|
76 lemma sfun_map_map: |
|
77 assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows |
|
78 "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
79 sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
80 unfolding sfun_map_def |
|
81 by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map) |
|
82 |
|
83 lemma ep_pair_sfun_map: |
|
84 assumes 1: "ep_pair e1 p1" |
|
85 assumes 2: "ep_pair e2 p2" |
|
86 shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)" |
|
87 proof |
|
88 interpret e1p1: pcpo_ep_pair e1 p1 |
|
89 unfolding pcpo_ep_pair_def by fact |
|
90 interpret e2p2: pcpo_ep_pair e2 p2 |
|
91 unfolding pcpo_ep_pair_def by fact |
|
92 fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" |
|
93 unfolding sfun_map_def |
|
94 apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel) |
|
95 apply (rule ep_pair.e_inverse) |
|
96 apply (rule ep_pair_cfun_map [OF 1 2]) |
|
97 done |
|
98 fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" |
|
99 unfolding sfun_map_def |
|
100 apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel) |
|
101 apply (rule ep_pair.e_p_below) |
|
102 apply (rule ep_pair_cfun_map [OF 1 2]) |
|
103 done |
|
104 qed |
|
105 |
|
106 lemma deflation_sfun_map [domain_deflation]: |
|
107 assumes 1: "deflation d1" |
|
108 assumes 2: "deflation d2" |
|
109 shows "deflation (sfun_map\<cdot>d1\<cdot>d2)" |
|
110 apply (simp add: sfun_map_def) |
|
111 apply (rule deflation.intro) |
|
112 apply simp |
|
113 apply (subst strictify_cancel) |
|
114 apply (simp add: cfun_map_def deflation_strict 1 2) |
|
115 apply (simp add: cfun_map_def deflation.idem 1 2) |
|
116 apply (simp add: sfun.e_below_iff [symmetric]) |
|
117 apply (subst strictify_cancel) |
|
118 apply (simp add: cfun_map_def deflation_strict 1 2) |
|
119 apply (rule deflation.below) |
|
120 apply (rule deflation_cfun_map [OF 1 2]) |
|
121 done |
|
122 |
|
123 lemma finite_deflation_sfun_map: |
|
124 assumes 1: "finite_deflation d1" |
|
125 assumes 2: "finite_deflation d2" |
|
126 shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)" |
|
127 proof (intro finite_deflation.intro finite_deflation_axioms.intro) |
|
128 interpret d1: finite_deflation d1 by fact |
|
129 interpret d2: finite_deflation d2 by fact |
|
130 have "deflation d1" and "deflation d2" by fact+ |
|
131 thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map) |
|
132 from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
|
133 by (rule finite_deflation_cfun_map) |
|
134 then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
|
135 by (rule finite_deflation.finite_fixes) |
|
136 moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)" |
|
137 by (rule inj_onI, simp) |
|
138 ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})" |
|
139 by (rule finite_vimageI) |
|
140 then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
|
141 unfolding sfun_map_def sfun.e_eq_iff [symmetric] |
|
142 by (simp add: strictify_cancel |
|
143 deflation_strict `deflation d1` `deflation d2`) |
|
144 qed |
|
145 |
|
146 subsection {* Strict function space is a bifinite domain *} |
|
147 |
|
148 definition |
|
149 sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)" |
|
150 where |
|
151 "sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
|
152 |
|
153 lemma sfun_approx: "approx_chain sfun_approx" |
|
154 proof (rule approx_chain.intro) |
|
155 show "chain (\<lambda>i. sfun_approx i)" |
|
156 unfolding sfun_approx_def by simp |
|
157 show "(\<Squnion>i. sfun_approx i) = ID" |
|
158 unfolding sfun_approx_def |
|
159 by (simp add: lub_distribs sfun_map_ID) |
|
160 show "\<And>i. finite_deflation (sfun_approx i)" |
|
161 unfolding sfun_approx_def |
|
162 by (intro finite_deflation_sfun_map finite_deflation_udom_approx) |
|
163 qed |
|
164 |
|
165 definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
|
166 where "sfun_defl = defl_fun2 sfun_approx sfun_map" |
|
167 |
|
168 lemma cast_sfun_defl: |
|
169 "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) = |
|
170 udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx" |
|
171 unfolding sfun_defl_def |
|
172 apply (rule cast_defl_fun2 [OF sfun_approx]) |
|
173 apply (erule (1) finite_deflation_sfun_map) |
|
174 done |
|
175 |
|
176 instantiation sfun :: ("domain", "domain") liftdomain |
|
177 begin |
|
178 |
|
179 definition |
|
180 "emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb" |
|
181 |
|
182 definition |
|
183 "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx" |
|
184 |
|
185 definition |
|
186 "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
|
187 |
|
188 definition |
|
189 "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb" |
|
190 |
|
191 definition |
|
192 "(liftprj :: udom \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj oo udom_prj u_approx" |
|
193 |
|
194 definition |
|
195 "liftdefl (t::('a \<rightarrow>! 'b) itself) = u_defl\<cdot>DEFL('a \<rightarrow>! 'b)" |
|
196 |
|
197 instance |
|
198 using liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def |
|
199 proof (rule liftdomain_class_intro) |
|
200 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
|
201 unfolding emb_sfun_def prj_sfun_def |
|
202 using ep_pair_udom [OF sfun_approx] |
|
203 by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj) |
|
204 next |
|
205 show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
|
206 unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl |
|
207 by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map) |
|
208 qed |
|
209 |
|
210 end |
|
211 |
|
212 lemma DEFL_sfun [domain_defl_simps]: |
|
213 "DEFL('a \<rightarrow>! 'b) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
|
214 by (rule defl_sfun_def) |
|
215 |
|
216 lemma isodefl_sfun [domain_isodefl]: |
|
217 "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
218 isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)" |
|
219 apply (rule isodeflI) |
|
220 apply (simp add: cast_sfun_defl cast_isodefl) |
|
221 apply (simp add: emb_sfun_def prj_sfun_def) |
|
222 apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation]) |
|
223 done |
|
224 |
|
225 setup {* |
|
226 Domain_Take_Proofs.add_map_function |
|
227 (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]) |
|
228 *} |
|
229 |
|
230 end |
|