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