author | huffman |
Wed, 06 Oct 2010 10:49:27 -0700 | |
changeset 39974 | b525988432e9 |
parent 37110 | 7ffdbc24b27f |
child 39986 | 38677db30cad |
permissions | -rw-r--r-- |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
1 |
(* Title: HOLCF/Library/Strict_Fun.thy |
35167 | 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 |
||
35427 | 15 |
type_notation (xsymbols) |
16 |
sfun (infixr "\<rightarrow>!" 0) |
|
35167 | 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: expand_cfun_eq 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: expand_cfun_eq 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: expand_cfun_below 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: "sfun_map\<cdot>ID\<cdot>ID = ID" |
|
73 |
unfolding sfun_map_def |
|
74 |
by (simp add: cfun_map_ID expand_cfun_eq) |
|
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: expand_cfun_eq 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: |
|
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 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
146 |
subsection {* Strict function space is an SFP domain *} |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
147 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
148 |
definition |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
149 |
sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
150 |
where |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
151 |
"sfun_approx = (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
35167 | 152 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
153 |
lemma sfun_approx: "approx_chain sfun_approx" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
154 |
proof (rule approx_chain.intro) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
155 |
show "chain (\<lambda>i. sfun_approx i)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
156 |
unfolding sfun_approx_def by simp |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
157 |
show "(\<Squnion>i. sfun_approx i) = ID" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
158 |
unfolding sfun_approx_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
159 |
by (simp add: lub_distribs sfun_map_ID) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
160 |
show "\<And>i. finite_deflation (sfun_approx i)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
161 |
unfolding sfun_approx_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
162 |
by (intro finite_deflation_sfun_map finite_deflation_udom_approx) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
163 |
qed |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
164 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
165 |
definition sfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
166 |
where "sfun_sfp = sfp_fun2 sfun_approx sfun_map" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
167 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
168 |
lemma cast_sfun_sfp: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
169 |
"cast\<cdot>(sfun_sfp\<cdot>A\<cdot>B) = |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
170 |
udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
171 |
unfolding sfun_sfp_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
172 |
apply (rule cast_sfp_fun2 [OF sfun_approx]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
173 |
apply (erule (1) finite_deflation_sfun_map) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
174 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
175 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
176 |
instantiation sfun :: (sfp, sfp) sfp |
35167 | 177 |
begin |
178 |
||
179 |
definition |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
180 |
"emb = udom_emb sfun_approx oo sfun_map\<cdot>prj\<cdot>emb" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
181 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
182 |
definition |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
183 |
"prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
184 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
185 |
definition |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
186 |
"sfp (t::('a \<rightarrow>! 'b) itself) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
35167 | 187 |
|
188 |
instance proof |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
189 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
190 |
unfolding emb_sfun_def prj_sfun_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
191 |
using ep_pair_udom [OF sfun_approx] |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
192 |
by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj) |
35167 | 193 |
next |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
194 |
show "cast\<cdot>SFP('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
195 |
unfolding emb_sfun_def prj_sfun_def sfp_sfun_def cast_sfun_sfp |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
196 |
by (simp add: cast_SFP oo_def expand_cfun_eq sfun_map_map) |
35167 | 197 |
qed |
198 |
||
199 |
end |
|
200 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
201 |
text {* SFP of type constructor = type combinator *} |
35167 | 202 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
203 |
lemma SFP_sfun: "SFP('a::sfp \<rightarrow>! 'b::sfp) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
204 |
by (rule sfp_sfun_def) |
35167 | 205 |
|
206 |
lemma isodefl_sfun: |
|
207 |
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
208 |
isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_sfp\<cdot>t1\<cdot>t2)" |
35167 | 209 |
apply (rule isodeflI) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
210 |
apply (simp add: cast_sfun_sfp cast_isodefl) |
35167 | 211 |
apply (simp add: emb_sfun_def prj_sfun_def) |
212 |
apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation]) |
|
213 |
done |
|
214 |
||
215 |
setup {* |
|
216 |
Domain_Isomorphism.add_type_constructor |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
217 |
(@{type_name "sfun"}, @{term sfun_sfp}, @{const_name sfun_map}, @{thm SFP_sfun}, |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35167
diff
changeset
|
218 |
@{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map}) |
35167 | 219 |
*} |
220 |
||
221 |
end |