author | huffman |
Wed, 27 Oct 2010 11:10:36 -0700 | |
changeset 40218 | f7d4d023a899 |
parent 40216 | 366309dfaf60 |
child 40487 | 1320a0747974 |
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" |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
40 |
by (simp add: cfun_eq_iff strictify_conv_if) |
35167 | 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) |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
46 |
apply (simp add: cfun_eq_iff strictify_conv_if) |
35167 | 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) |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
59 |
apply (simp add: cfun_below_iff strictify_conv_if) |
35167 | 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 |
||
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40002
diff
changeset
|
72 |
lemma sfun_map_ID [domain_map_ID]: "sfun_map\<cdot>ID\<cdot>ID = ID" |
35167 | 73 |
unfolding sfun_map_def |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
74 |
by (simp add: cfun_map_ID cfun_eq_iff) |
35167 | 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 |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
81 |
by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map) |
35167 | 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 |
||
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40002
diff
changeset
|
106 |
lemma deflation_sfun_map [domain_deflation]: |
35167 | 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 |
||
39986 | 146 |
subsection {* Strict function space is a bifinite domain *} |
39974
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 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
165 |
definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
166 |
where "sfun_defl = defl_fun2 sfun_approx sfun_map" |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
37110
diff
changeset
|
167 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
168 |
lemma cast_sfun_defl: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
169 |
"cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) = |
39974
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" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
171 |
unfolding sfun_defl_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
172 |
apply (rule cast_defl_fun2 [OF sfun_approx]) |
39974
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 |
|
39986 | 176 |
instantiation sfun :: (bifinite, bifinite) bifinite |
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 |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
186 |
"defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('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 |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
194 |
show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
195 |
unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
196 |
by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map) |
35167 | 197 |
qed |
198 |
||
199 |
end |
|
200 |
||
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40002
diff
changeset
|
201 |
lemma DEFL_sfun [domain_defl_simps]: |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
202 |
"DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
203 |
by (rule defl_sfun_def) |
35167 | 204 |
|
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40002
diff
changeset
|
205 |
lemma isodefl_sfun [domain_isodefl]: |
35167 | 206 |
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
207 |
isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)" |
35167 | 208 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
209 |
apply (simp add: cast_sfun_defl cast_isodefl) |
35167 | 210 |
apply (simp add: emb_sfun_def prj_sfun_def) |
211 |
apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation]) |
|
212 |
done |
|
213 |
||
214 |
setup {* |
|
215 |
Domain_Isomorphism.add_type_constructor |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
216 |
(@{type_name "sfun"}, @{const_name sfun_defl}, @{const_name sfun_map}, [true, true]) |
35167 | 217 |
*} |
218 |
||
219 |
end |