author | huffman |
Fri, 22 May 2009 10:34:22 -0700 | |
changeset 31230 | 50deb3badfba |
parent 31076 | 99fe356cbbc2 |
child 32126 | a5042f260440 |
permissions | -rw-r--r-- |
15741 | 1 |
(* Title: HOLCF/Domain.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Domain package *} |
|
6 |
||
7 |
theory Domain |
|
16230 | 8 |
imports Ssum Sprod Up One Tr Fixrec |
30910 | 9 |
uses |
10 |
("Tools/cont_consts.ML") |
|
11 |
("Tools/cont_proc.ML") |
|
12 |
("Tools/domain/domain_library.ML") |
|
13 |
("Tools/domain/domain_syntax.ML") |
|
14 |
("Tools/domain/domain_axioms.ML") |
|
15 |
("Tools/domain/domain_theorems.ML") |
|
16 |
("Tools/domain/domain_extender.ML") |
|
15741 | 17 |
begin |
18 |
||
19 |
defaultsort pcpo |
|
20 |
||
23376 | 21 |
|
15741 | 22 |
subsection {* Continuous isomorphisms *} |
23 |
||
24 |
text {* A locale for continuous isomorphisms *} |
|
25 |
||
26 |
locale iso = |
|
27 |
fixes abs :: "'a \<rightarrow> 'b" |
|
28 |
fixes rep :: "'b \<rightarrow> 'a" |
|
29 |
assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x" |
|
30 |
assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y" |
|
23376 | 31 |
begin |
15741 | 32 |
|
23376 | 33 |
lemma swap: "iso rep abs" |
34 |
by (rule iso.intro [OF rep_iso abs_iso]) |
|
15741 | 35 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30911
diff
changeset
|
36 |
lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)" |
17835 | 37 |
proof |
38 |
assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" |
|
23376 | 39 |
then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg) |
40 |
then show "x \<sqsubseteq> y" by simp |
|
17835 | 41 |
next |
42 |
assume "x \<sqsubseteq> y" |
|
23376 | 43 |
then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg) |
17835 | 44 |
qed |
45 |
||
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30911
diff
changeset
|
46 |
lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)" |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30911
diff
changeset
|
47 |
by (rule iso.abs_below [OF swap]) |
17835 | 48 |
|
23376 | 49 |
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30911
diff
changeset
|
50 |
by (simp add: po_eq_conv abs_below) |
17835 | 51 |
|
23376 | 52 |
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)" |
53 |
by (rule iso.abs_eq [OF swap]) |
|
17835 | 54 |
|
23376 | 55 |
lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>" |
15741 | 56 |
proof - |
57 |
have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" .. |
|
23376 | 58 |
then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg) |
59 |
then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp |
|
60 |
then show ?thesis by (rule UU_I) |
|
15741 | 61 |
qed |
62 |
||
23376 | 63 |
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>" |
64 |
by (rule iso.abs_strict [OF swap]) |
|
15741 | 65 |
|
23376 | 66 |
lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>" |
15741 | 67 |
proof - |
17835 | 68 |
have "x = rep\<cdot>(abs\<cdot>x)" by simp |
69 |
also assume "abs\<cdot>x = \<bottom>" |
|
15741 | 70 |
also note rep_strict |
17835 | 71 |
finally show "x = \<bottom>" . |
15741 | 72 |
qed |
73 |
||
23376 | 74 |
lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>" |
75 |
by (rule iso.abs_defin' [OF swap]) |
|
15741 | 76 |
|
23376 | 77 |
lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>" |
78 |
by (erule contrapos_nn, erule abs_defin') |
|
15741 | 79 |
|
23376 | 80 |
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>" |
81 |
by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms) |
|
17835 | 82 |
|
23376 | 83 |
lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)" |
84 |
by (auto elim: abs_defin' intro: abs_strict) |
|
17835 | 85 |
|
23376 | 86 |
lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)" |
87 |
by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms) |
|
15741 | 88 |
|
17836 | 89 |
lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" |
90 |
proof (unfold compact_def) |
|
91 |
assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)" |
|
92 |
with cont_Rep_CFun2 |
|
93 |
have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst) |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30911
diff
changeset
|
94 |
then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp |
17836 | 95 |
qed |
96 |
||
23376 | 97 |
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x" |
98 |
by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms) |
|
17836 | 99 |
|
23376 | 100 |
lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)" |
101 |
by (rule compact_rep_rev) simp |
|
17836 | 102 |
|
23376 | 103 |
lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)" |
104 |
by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms) |
|
17836 | 105 |
|
23376 | 106 |
lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)" |
15741 | 107 |
proof |
108 |
assume "x = abs\<cdot>y" |
|
23376 | 109 |
then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp |
110 |
then show "rep\<cdot>x = y" by simp |
|
15741 | 111 |
next |
112 |
assume "rep\<cdot>x = y" |
|
23376 | 113 |
then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp |
114 |
then show "x = abs\<cdot>y" by simp |
|
15741 | 115 |
qed |
116 |
||
23376 | 117 |
end |
118 |
||
119 |
||
15741 | 120 |
subsection {* Casedist *} |
121 |
||
122 |
lemma ex_one_defined_iff: |
|
123 |
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE" |
|
124 |
apply safe |
|
125 |
apply (rule_tac p=x in oneE) |
|
126 |
apply simp |
|
127 |
apply simp |
|
128 |
apply force |
|
23376 | 129 |
done |
15741 | 130 |
|
131 |
lemma ex_up_defined_iff: |
|
132 |
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))" |
|
133 |
apply safe |
|
16754 | 134 |
apply (rule_tac p=x in upE) |
15741 | 135 |
apply simp |
136 |
apply fast |
|
16320 | 137 |
apply (force intro!: up_defined) |
23376 | 138 |
done |
15741 | 139 |
|
140 |
lemma ex_sprod_defined_iff: |
|
141 |
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
|
142 |
(\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)" |
|
143 |
apply safe |
|
144 |
apply (rule_tac p=y in sprodE) |
|
145 |
apply simp |
|
146 |
apply fast |
|
16217 | 147 |
apply (force intro!: spair_defined) |
23376 | 148 |
done |
15741 | 149 |
|
150 |
lemma ex_sprod_up_defined_iff: |
|
151 |
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
|
152 |
(\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)" |
|
153 |
apply safe |
|
154 |
apply (rule_tac p=y in sprodE) |
|
155 |
apply simp |
|
16754 | 156 |
apply (rule_tac p=x in upE) |
15741 | 157 |
apply simp |
158 |
apply fast |
|
16217 | 159 |
apply (force intro!: spair_defined) |
23376 | 160 |
done |
15741 | 161 |
|
162 |
lemma ex_ssum_defined_iff: |
|
163 |
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = |
|
164 |
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or> |
|
165 |
(\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))" |
|
166 |
apply (rule iffI) |
|
167 |
apply (erule exE) |
|
168 |
apply (erule conjE) |
|
169 |
apply (rule_tac p=x in ssumE) |
|
170 |
apply simp |
|
171 |
apply (rule disjI1, fast) |
|
172 |
apply (rule disjI2, fast) |
|
173 |
apply (erule disjE) |
|
17835 | 174 |
apply force |
175 |
apply force |
|
23376 | 176 |
done |
15741 | 177 |
|
178 |
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)" |
|
23376 | 179 |
by auto |
15741 | 180 |
|
181 |
lemmas ex_defined_iffs = |
|
182 |
ex_ssum_defined_iff |
|
183 |
ex_sprod_up_defined_iff |
|
184 |
ex_sprod_defined_iff |
|
185 |
ex_up_defined_iff |
|
186 |
ex_one_defined_iff |
|
187 |
||
188 |
text {* Rules for turning exh into casedist *} |
|
189 |
||
190 |
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *) |
|
23376 | 191 |
by auto |
15741 | 192 |
|
193 |
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)" |
|
23376 | 194 |
by rule auto |
15741 | 195 |
|
196 |
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)" |
|
23376 | 197 |
by rule auto |
15741 | 198 |
|
199 |
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)" |
|
23376 | 200 |
by rule auto |
15741 | 201 |
|
202 |
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 |
|
203 |
||
30910 | 204 |
|
31230 | 205 |
subsection {* Combinators for building copy functions *} |
206 |
||
207 |
definition |
|
208 |
cfun_fun :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)" |
|
209 |
where |
|
210 |
"cfun_fun = (\<Lambda> f g p. g oo p oo f)" |
|
211 |
||
212 |
definition |
|
213 |
ssum_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd" |
|
214 |
where |
|
215 |
"ssum_fun = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))" |
|
216 |
||
217 |
definition |
|
218 |
sprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd" |
|
219 |
where |
|
220 |
"sprod_fun = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))" |
|
221 |
||
222 |
definition |
|
223 |
cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd" |
|
224 |
where |
|
225 |
"cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. <f\<cdot>x, g\<cdot>y>))" |
|
226 |
||
227 |
definition |
|
228 |
u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u" |
|
229 |
where |
|
230 |
"u_fun = (\<Lambda> f. fup\<cdot>(up oo f))" |
|
231 |
||
232 |
lemma cfun_fun_strict: "b\<cdot>\<bottom> = \<bottom> \<Longrightarrow> cfun_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
|
233 |
unfolding cfun_fun_def expand_cfun_eq by simp |
|
234 |
||
235 |
lemma ssum_fun_strict: "ssum_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
|
236 |
unfolding ssum_fun_def by simp |
|
237 |
||
238 |
lemma sprod_fun_strict: "sprod_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
|
239 |
unfolding sprod_fun_def by simp |
|
240 |
||
241 |
lemma u_fun_strict: "u_fun\<cdot>a\<cdot>\<bottom> = \<bottom>" |
|
242 |
unfolding u_fun_def by simp |
|
243 |
||
244 |
lemma ssum_fun_sinl: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
|
245 |
by (simp add: ssum_fun_def) |
|
246 |
||
247 |
lemma ssum_fun_sinr: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
|
248 |
by (simp add: ssum_fun_def) |
|
249 |
||
250 |
lemma sprod_fun_spair: |
|
251 |
"x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_fun\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
|
252 |
by (simp add: sprod_fun_def) |
|
253 |
||
254 |
lemma u_fun_up: "u_fun\<cdot>a\<cdot>(up\<cdot>x) = up\<cdot>(a\<cdot>x)" |
|
255 |
by (simp add: u_fun_def) |
|
256 |
||
257 |
lemmas domain_fun_stricts = |
|
258 |
ssum_fun_strict sprod_fun_strict u_fun_strict |
|
259 |
||
260 |
lemmas domain_fun_simps = |
|
261 |
ssum_fun_sinl ssum_fun_sinr sprod_fun_spair u_fun_up |
|
262 |
||
263 |
||
30910 | 264 |
subsection {* Installing the domain package *} |
265 |
||
30911
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
266 |
lemmas con_strict_rules = |
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
267 |
sinl_strict sinr_strict spair_strict1 spair_strict2 |
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
268 |
|
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
269 |
lemmas con_defin_rules = |
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
270 |
sinl_defined sinr_defined spair_defined up_defined ONE_defined |
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
271 |
|
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
272 |
lemmas con_defined_iff_rules = |
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
273 |
sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined |
7809cbaa1b61
domain package: simplify internal proofs of con_rews
huffman
parents:
30910
diff
changeset
|
274 |
|
30910 | 275 |
use "Tools/cont_consts.ML" |
276 |
use "Tools/cont_proc.ML" |
|
277 |
use "Tools/domain/domain_library.ML" |
|
278 |
use "Tools/domain/domain_syntax.ML" |
|
279 |
use "Tools/domain/domain_axioms.ML" |
|
280 |
use "Tools/domain/domain_theorems.ML" |
|
281 |
use "Tools/domain/domain_extender.ML" |
|
282 |
||
15741 | 283 |
end |