author | huffman |
Fri, 05 Mar 2010 14:05:25 -0800 | |
changeset 35596 | 49a02dab35ed |
parent 35595 | 1785d387627a |
child 35652 | 05ca920cd94b |
permissions | -rw-r--r-- |
33589 | 1 |
(* Title: HOLCF/Representable.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
33588 | 5 |
header {* Representable Types *} |
6 |
||
7 |
theory Representable |
|
35473 | 8 |
imports Algebraic Universal Ssum Sprod One Fixrec |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
9 |
uses |
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
10 |
("Tools/repdef.ML") |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35490
diff
changeset
|
11 |
("Tools/Domain/domain_take_proofs.ML") |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
12 |
("Tools/Domain/domain_isomorphism.ML") |
33588 | 13 |
begin |
14 |
||
35595 | 15 |
subsection {* Preliminaries: Take proofs *} |
16 |
||
35596 | 17 |
text {* |
18 |
This section contains lemmas that are used in a module that supports |
|
19 |
the domain isomorphism package; the module contains proofs related |
|
20 |
to take functions and the finiteness predicate. |
|
21 |
*} |
|
22 |
||
35595 | 23 |
lemma deflation_abs_rep: |
24 |
fixes abs and rep and d |
|
25 |
assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" |
|
26 |
assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" |
|
27 |
shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" |
|
28 |
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) |
|
29 |
||
30 |
lemma deflation_chain_min: |
|
31 |
assumes chain: "chain d" |
|
32 |
assumes defl: "\<And>n. deflation (d n)" |
|
33 |
shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x" |
|
34 |
proof (rule linorder_le_cases) |
|
35 |
assume "m \<le> n" |
|
36 |
with chain have "d m \<sqsubseteq> d n" by (rule chain_mono) |
|
37 |
then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x" |
|
38 |
by (rule deflation_below_comp1 [OF defl defl]) |
|
39 |
moreover from `m \<le> n` have "min m n = m" by simp |
|
40 |
ultimately show ?thesis by simp |
|
41 |
next |
|
42 |
assume "n \<le> m" |
|
43 |
with chain have "d n \<sqsubseteq> d m" by (rule chain_mono) |
|
44 |
then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x" |
|
45 |
by (rule deflation_below_comp2 [OF defl defl]) |
|
46 |
moreover from `n \<le> m` have "min m n = n" by simp |
|
47 |
ultimately show ?thesis by simp |
|
48 |
qed |
|
49 |
||
50 |
use "Tools/Domain/domain_take_proofs.ML" |
|
51 |
||
52 |
||
33588 | 53 |
subsection {* Class of representable types *} |
54 |
||
55 |
text "Overloaded embedding and projection functions between |
|
56 |
a representable type and the universal domain." |
|
57 |
||
58 |
class rep = bifinite + |
|
59 |
fixes emb :: "'a::pcpo \<rightarrow> udom" |
|
60 |
fixes prj :: "udom \<rightarrow> 'a::pcpo" |
|
61 |
assumes ep_pair_emb_prj: "ep_pair emb prj" |
|
62 |
||
63 |
interpretation rep!: |
|
64 |
pcpo_ep_pair |
|
65 |
"emb :: 'a::rep \<rightarrow> udom" |
|
66 |
"prj :: udom \<rightarrow> 'a::rep" |
|
67 |
unfolding pcpo_ep_pair_def |
|
68 |
by (rule ep_pair_emb_prj) |
|
69 |
||
70 |
lemmas emb_inverse = rep.e_inverse |
|
71 |
lemmas emb_prj_below = rep.e_p_below |
|
72 |
lemmas emb_eq_iff = rep.e_eq_iff |
|
73 |
lemmas emb_strict = rep.e_strict |
|
74 |
lemmas prj_strict = rep.p_strict |
|
75 |
||
76 |
||
77 |
subsection {* Making @{term rep} the default class *} |
|
78 |
||
79 |
text {* |
|
80 |
From now on, free type variables are assumed to be in class |
|
81 |
@{term rep}, unless specified otherwise. |
|
82 |
*} |
|
83 |
||
84 |
defaultsort rep |
|
85 |
||
86 |
subsection {* Representations of types *} |
|
87 |
||
88 |
text "A TypeRep is an algebraic deflation over the universe of values." |
|
89 |
||
90 |
types TypeRep = "udom alg_defl" |
|
35431 | 91 |
translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl" |
33588 | 92 |
|
93 |
definition |
|
94 |
Rep_of :: "'a::rep itself \<Rightarrow> TypeRep" |
|
95 |
where |
|
96 |
"Rep_of TYPE('a::rep) = |
|
97 |
(\<Squnion>i. alg_defl_principal (Abs_fin_defl |
|
98 |
(emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))" |
|
99 |
||
100 |
syntax "_REP" :: "type \<Rightarrow> TypeRep" ("(1REP/(1'(_')))") |
|
35431 | 101 |
translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)" |
33588 | 102 |
|
103 |
lemma cast_REP: |
|
104 |
"cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)" |
|
105 |
proof - |
|
106 |
let ?a = "\<lambda>i. emb oo approx i oo (prj::udom \<rightarrow> 'a)" |
|
107 |
have a: "\<And>i. finite_deflation (?a i)" |
|
108 |
apply (rule rep.finite_deflation_e_d_p) |
|
109 |
apply (rule finite_deflation_approx) |
|
110 |
done |
|
111 |
show ?thesis |
|
112 |
unfolding Rep_of_def |
|
113 |
apply (subst contlub_cfun_arg) |
|
114 |
apply (rule chainI) |
|
115 |
apply (rule alg_defl.principal_mono) |
|
116 |
apply (rule Abs_fin_defl_mono [OF a a]) |
|
117 |
apply (rule chainE, simp) |
|
118 |
apply (subst cast_alg_defl_principal) |
|
119 |
apply (simp add: Abs_fin_defl_inverse a) |
|
120 |
apply (simp add: expand_cfun_eq lub_distribs) |
|
121 |
done |
|
122 |
qed |
|
123 |
||
124 |
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::rep) = cast\<cdot>REP('a)\<cdot>x" |
|
125 |
by (simp add: cast_REP) |
|
126 |
||
127 |
lemma in_REP_iff: |
|
128 |
"x ::: REP('a::rep) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x" |
|
129 |
by (simp add: in_deflation_def cast_REP) |
|
130 |
||
131 |
lemma prj_inverse: |
|
132 |
"x ::: REP('a::rep) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x" |
|
133 |
by (simp only: in_REP_iff) |
|
134 |
||
135 |
lemma emb_in_REP [simp]: |
|
136 |
"emb\<cdot>(x::'a::rep) ::: REP('a)" |
|
137 |
by (simp add: in_REP_iff) |
|
138 |
||
139 |
subsection {* Coerce operator *} |
|
140 |
||
141 |
definition coerce :: "'a \<rightarrow> 'b" |
|
142 |
where "coerce = prj oo emb" |
|
143 |
||
144 |
lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)" |
|
145 |
by (simp add: coerce_def) |
|
146 |
||
147 |
lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x" |
|
148 |
by (simp add: coerce_def) |
|
149 |
||
150 |
lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>" |
|
151 |
by (simp add: coerce_def) |
|
152 |
||
153 |
lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID" |
|
154 |
by (rule ext_cfun, simp add: beta_coerce) |
|
155 |
||
156 |
lemma emb_coerce: |
|
157 |
"REP('a) \<sqsubseteq> REP('b) |
|
158 |
\<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x" |
|
159 |
apply (simp add: beta_coerce) |
|
160 |
apply (rule prj_inverse) |
|
161 |
apply (erule subdeflationD) |
|
162 |
apply (rule emb_in_REP) |
|
163 |
done |
|
164 |
||
165 |
lemma coerce_prj: |
|
166 |
"REP('a) \<sqsubseteq> REP('b) |
|
167 |
\<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x" |
|
168 |
apply (simp add: coerce_def) |
|
169 |
apply (rule emb_eq_iff [THEN iffD1]) |
|
170 |
apply (simp only: emb_prj) |
|
171 |
apply (rule deflation_below_comp1) |
|
172 |
apply (rule deflation_cast) |
|
173 |
apply (rule deflation_cast) |
|
174 |
apply (erule monofun_cfun_arg) |
|
175 |
done |
|
176 |
||
177 |
lemma coerce_coerce [simp]: |
|
178 |
"REP('a) \<sqsubseteq> REP('b) |
|
179 |
\<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x" |
|
180 |
by (simp add: beta_coerce prj_inverse subdeflationD) |
|
181 |
||
182 |
lemma coerce_inverse: |
|
183 |
"emb\<cdot>(x::'a) ::: REP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x" |
|
184 |
by (simp only: beta_coerce prj_inverse emb_inverse) |
|
185 |
||
186 |
lemma coerce_type: |
|
187 |
"REP('a) \<sqsubseteq> REP('b) |
|
188 |
\<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: REP('a)" |
|
189 |
by (simp add: beta_coerce prj_inverse subdeflationD) |
|
190 |
||
191 |
lemma ep_pair_coerce: |
|
192 |
"REP('a) \<sqsubseteq> REP('b) |
|
193 |
\<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)" |
|
194 |
apply (rule ep_pair.intro) |
|
195 |
apply simp |
|
196 |
apply (simp only: beta_coerce) |
|
197 |
apply (rule below_trans) |
|
198 |
apply (rule monofun_cfun_arg) |
|
199 |
apply (rule emb_prj_below) |
|
200 |
apply simp |
|
201 |
done |
|
202 |
||
33779 | 203 |
text {* Isomorphism lemmas used internally by the domain package: *} |
204 |
||
205 |
lemma domain_abs_iso: |
|
206 |
fixes abs and rep |
|
207 |
assumes REP: "REP('b) = REP('a)" |
|
208 |
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)" |
|
209 |
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)" |
|
210 |
shows "rep\<cdot>(abs\<cdot>x) = x" |
|
211 |
unfolding abs_def rep_def by (simp add: REP) |
|
212 |
||
213 |
lemma domain_rep_iso: |
|
214 |
fixes abs and rep |
|
215 |
assumes REP: "REP('b) = REP('a)" |
|
216 |
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)" |
|
217 |
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)" |
|
218 |
shows "abs\<cdot>(rep\<cdot>x) = x" |
|
219 |
unfolding abs_def rep_def by (simp add: REP [symmetric]) |
|
220 |
||
221 |
||
33588 | 222 |
subsection {* Proving a subtype is representable *} |
223 |
||
224 |
text {* |
|
225 |
Temporarily relax type constraints for @{term "approx"}, |
|
226 |
@{term emb}, and @{term prj}. |
|
227 |
*} |
|
228 |
||
229 |
setup {* Sign.add_const_constraint |
|
230 |
(@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::cpo \<rightarrow> 'a"}) *} |
|
231 |
||
232 |
setup {* Sign.add_const_constraint |
|
233 |
(@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *} |
|
234 |
||
235 |
setup {* Sign.add_const_constraint |
|
236 |
(@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *} |
|
237 |
||
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
238 |
definition |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
239 |
repdef_approx :: |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
240 |
"('a::pcpo \<Rightarrow> udom) \<Rightarrow> (udom \<Rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> nat \<Rightarrow> 'a \<rightarrow> 'a" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
241 |
where |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
242 |
"repdef_approx Rep Abs t = (\<lambda>i. \<Lambda> x. Abs (cast\<cdot>(approx i\<cdot>t)\<cdot>(Rep x)))" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
243 |
|
33588 | 244 |
lemma typedef_rep_class: |
245 |
fixes Rep :: "'a::pcpo \<Rightarrow> udom" |
|
246 |
fixes Abs :: "udom \<Rightarrow> 'a::pcpo" |
|
247 |
fixes t :: TypeRep |
|
248 |
assumes type: "type_definition Rep Abs {x. x ::: t}" |
|
249 |
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
250 |
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
251 |
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
252 |
assumes approx: "(approx :: nat \<Rightarrow> 'a \<rightarrow> 'a) \<equiv> repdef_approx Rep Abs t" |
33588 | 253 |
shows "OFCLASS('a, rep_class)" |
254 |
proof |
|
255 |
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})" |
|
256 |
by (simp add: adm_in_deflation) |
|
257 |
have emb_beta: "\<And>x. emb\<cdot>x = Rep x" |
|
258 |
unfolding emb |
|
259 |
apply (rule beta_cfun) |
|
260 |
apply (rule typedef_cont_Rep [OF type below adm]) |
|
261 |
done |
|
262 |
have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)" |
|
263 |
unfolding prj |
|
264 |
apply (rule beta_cfun) |
|
265 |
apply (rule typedef_cont_Abs [OF type below adm]) |
|
266 |
apply simp_all |
|
267 |
done |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
268 |
have cast_cast_approx: |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
269 |
"\<And>i x. cast\<cdot>t\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>x) = cast\<cdot>(approx i\<cdot>t)\<cdot>x" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
270 |
apply (rule cast_fixed) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
271 |
apply (rule subdeflationD) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
272 |
apply (rule approx.below) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
273 |
apply (rule cast_in_deflation) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
274 |
done |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
275 |
have approx': |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
276 |
"approx = (\<lambda>i. \<Lambda>(x::'a). prj\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>(emb\<cdot>x)))" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
277 |
unfolding approx repdef_approx_def |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
278 |
apply (subst cast_cast_approx [symmetric]) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
279 |
apply (simp add: prj_beta [symmetric] emb_beta [symmetric]) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
280 |
done |
33588 | 281 |
have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t" |
282 |
using type_definition.Rep [OF type] |
|
283 |
by (simp add: emb_beta) |
|
284 |
have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x" |
|
285 |
unfolding prj_beta |
|
286 |
apply (simp add: cast_fixed [OF emb_in_deflation]) |
|
287 |
apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) |
|
288 |
done |
|
289 |
have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y" |
|
290 |
unfolding prj_beta emb_beta |
|
291 |
by (simp add: type_definition.Abs_inverse [OF type]) |
|
292 |
show "ep_pair (emb :: 'a \<rightarrow> udom) prj" |
|
293 |
apply default |
|
294 |
apply (simp add: prj_emb) |
|
295 |
apply (simp add: emb_prj cast.below) |
|
296 |
done |
|
297 |
show "chain (approx :: nat \<Rightarrow> 'a \<rightarrow> 'a)" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
298 |
unfolding approx' by simp |
33588 | 299 |
show "\<And>x::'a. (\<Squnion>i. approx i\<cdot>x) = x" |
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
300 |
unfolding approx' |
33588 | 301 |
apply (simp add: lub_distribs) |
302 |
apply (subst cast_fixed [OF emb_in_deflation]) |
|
303 |
apply (rule prj_emb) |
|
304 |
done |
|
305 |
show "\<And>(i::nat) (x::'a). approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
306 |
unfolding approx' |
33588 | 307 |
apply simp |
308 |
apply (simp add: emb_prj) |
|
309 |
apply (simp add: cast_cast_approx) |
|
310 |
done |
|
311 |
show "\<And>i::nat. finite {x::'a. approx i\<cdot>x = x}" |
|
312 |
apply (rule_tac B="(\<lambda>x. prj\<cdot>x) ` {x. cast\<cdot>(approx i\<cdot>t)\<cdot>x = x}" |
|
313 |
in finite_subset) |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
314 |
apply (clarsimp simp add: approx') |
33588 | 315 |
apply (drule_tac f="\<lambda>x. emb\<cdot>x" in arg_cong) |
316 |
apply (rule image_eqI) |
|
317 |
apply (rule prj_emb [symmetric]) |
|
318 |
apply (simp add: emb_prj) |
|
319 |
apply (simp add: cast_cast_approx) |
|
320 |
apply (rule finite_imageI) |
|
321 |
apply (simp add: cast_approx_fixed_iff) |
|
322 |
apply (simp add: Collect_conj_eq) |
|
323 |
apply (simp add: finite_fixes_approx) |
|
324 |
done |
|
325 |
qed |
|
326 |
||
327 |
text {* Restore original typing constraints *} |
|
328 |
||
329 |
setup {* Sign.add_const_constraint |
|
330 |
(@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::profinite \<rightarrow> 'a"}) *} |
|
331 |
||
332 |
setup {* Sign.add_const_constraint |
|
333 |
(@{const_name emb}, SOME @{typ "'a::rep \<rightarrow> udom"}) *} |
|
334 |
||
335 |
setup {* Sign.add_const_constraint |
|
336 |
(@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::rep"}) *} |
|
337 |
||
338 |
lemma typedef_REP: |
|
339 |
fixes Rep :: "'a::rep \<Rightarrow> udom" |
|
340 |
fixes Abs :: "udom \<Rightarrow> 'a::rep" |
|
341 |
fixes t :: TypeRep |
|
342 |
assumes type: "type_definition Rep Abs {x. x ::: t}" |
|
343 |
assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
344 |
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
345 |
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))" |
33588 | 346 |
shows "REP('a) = t" |
347 |
proof - |
|
348 |
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})" |
|
349 |
by (simp add: adm_in_deflation) |
|
350 |
have emb_beta: "\<And>x. emb\<cdot>x = Rep x" |
|
351 |
unfolding emb |
|
352 |
apply (rule beta_cfun) |
|
353 |
apply (rule typedef_cont_Rep [OF type below adm]) |
|
354 |
done |
|
355 |
have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)" |
|
356 |
unfolding prj |
|
357 |
apply (rule beta_cfun) |
|
358 |
apply (rule typedef_cont_Abs [OF type below adm]) |
|
359 |
apply simp_all |
|
360 |
done |
|
361 |
have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t" |
|
362 |
using type_definition.Rep [OF type] |
|
363 |
by (simp add: emb_beta) |
|
364 |
have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x" |
|
365 |
unfolding prj_beta |
|
366 |
apply (simp add: cast_fixed [OF emb_in_deflation]) |
|
367 |
apply (simp add: emb_beta type_definition.Rep_inverse [OF type]) |
|
368 |
done |
|
369 |
have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y" |
|
370 |
unfolding prj_beta emb_beta |
|
371 |
by (simp add: type_definition.Abs_inverse [OF type]) |
|
372 |
show "REP('a) = t" |
|
373 |
apply (rule cast_eq_imp_eq, rule ext_cfun) |
|
374 |
apply (simp add: cast_REP emb_prj) |
|
375 |
done |
|
376 |
qed |
|
377 |
||
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
378 |
lemma adm_mem_Collect_in_deflation: "adm (\<lambda>x. x \<in> {x. x ::: A})" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
379 |
unfolding mem_Collect_eq by (rule adm_in_deflation) |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
380 |
|
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
381 |
use "Tools/repdef.ML" |
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33589
diff
changeset
|
382 |
|
33588 | 383 |
|
384 |
subsection {* Instances of class @{text rep} *} |
|
385 |
||
386 |
subsubsection {* Universal Domain *} |
|
387 |
||
388 |
text "The Universal Domain itself is trivially representable." |
|
389 |
||
390 |
instantiation udom :: rep |
|
391 |
begin |
|
392 |
||
393 |
definition emb_udom_def [simp]: "emb = (ID :: udom \<rightarrow> udom)" |
|
394 |
definition prj_udom_def [simp]: "prj = (ID :: udom \<rightarrow> udom)" |
|
395 |
||
396 |
instance |
|
397 |
apply (intro_classes) |
|
398 |
apply (simp_all add: ep_pair.intro) |
|
399 |
done |
|
400 |
||
401 |
end |
|
402 |
||
403 |
subsubsection {* Lifted types *} |
|
404 |
||
405 |
instantiation lift :: (countable) rep |
|
406 |
begin |
|
407 |
||
408 |
definition emb_lift_def: |
|
409 |
"emb = udom_emb oo (FLIFT x. Def (to_nat x))" |
|
410 |
||
411 |
definition prj_lift_def: |
|
412 |
"prj = (FLIFT n. if (\<exists>x::'a::countable. n = to_nat x) |
|
413 |
then Def (THE x::'a. n = to_nat x) else \<bottom>) oo udom_prj" |
|
414 |
||
415 |
instance |
|
416 |
apply (intro_classes, unfold emb_lift_def prj_lift_def) |
|
417 |
apply (rule ep_pair_comp [OF _ ep_pair_udom]) |
|
418 |
apply (rule ep_pair.intro) |
|
419 |
apply (case_tac x, simp, simp) |
|
420 |
apply (case_tac y, simp, clarsimp) |
|
421 |
done |
|
422 |
||
423 |
end |
|
424 |
||
425 |
subsubsection {* Representable type constructors *} |
|
426 |
||
427 |
text "Functions between representable types are representable." |
|
428 |
||
35525 | 429 |
instantiation cfun :: (rep, rep) rep |
33588 | 430 |
begin |
431 |
||
432 |
definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb" |
|
433 |
definition prj_cfun_def: "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj" |
|
434 |
||
435 |
instance |
|
436 |
apply (intro_classes, unfold emb_cfun_def prj_cfun_def) |
|
437 |
apply (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj ep_pair_udom) |
|
438 |
done |
|
439 |
||
440 |
end |
|
441 |
||
442 |
text "Strict products of representable types are representable." |
|
443 |
||
35525 | 444 |
instantiation sprod :: (rep, rep) rep |
33588 | 445 |
begin |
446 |
||
447 |
definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb" |
|
448 |
definition prj_sprod_def: "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj" |
|
449 |
||
450 |
instance |
|
451 |
apply (intro_classes, unfold emb_sprod_def prj_sprod_def) |
|
452 |
apply (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj ep_pair_udom) |
|
453 |
done |
|
454 |
||
455 |
end |
|
456 |
||
457 |
text "Strict sums of representable types are representable." |
|
458 |
||
35525 | 459 |
instantiation ssum :: (rep, rep) rep |
33588 | 460 |
begin |
461 |
||
462 |
definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb" |
|
463 |
definition prj_ssum_def: "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj" |
|
464 |
||
465 |
instance |
|
466 |
apply (intro_classes, unfold emb_ssum_def prj_ssum_def) |
|
467 |
apply (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj ep_pair_udom) |
|
468 |
done |
|
469 |
||
470 |
end |
|
471 |
||
472 |
text "Up of a representable type is representable." |
|
473 |
||
474 |
instantiation "u" :: (rep) rep |
|
475 |
begin |
|
476 |
||
477 |
definition emb_u_def: "emb = udom_emb oo u_map\<cdot>emb" |
|
478 |
definition prj_u_def: "prj = u_map\<cdot>prj oo udom_prj" |
|
479 |
||
480 |
instance |
|
481 |
apply (intro_classes, unfold emb_u_def prj_u_def) |
|
482 |
apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj ep_pair_udom) |
|
483 |
done |
|
484 |
||
485 |
end |
|
486 |
||
487 |
text "Cartesian products of representable types are representable." |
|
488 |
||
489 |
instantiation "*" :: (rep, rep) rep |
|
490 |
begin |
|
491 |
||
492 |
definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb" |
|
493 |
definition prj_cprod_def: "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj" |
|
494 |
||
495 |
instance |
|
496 |
apply (intro_classes, unfold emb_cprod_def prj_cprod_def) |
|
497 |
apply (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj ep_pair_udom) |
|
498 |
done |
|
499 |
||
500 |
end |
|
501 |
||
502 |
subsection {* Type combinators *} |
|
503 |
||
504 |
definition |
|
505 |
TypeRep_fun1 :: |
|
506 |
"((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) |
|
507 |
\<Rightarrow> (TypeRep \<rightarrow> TypeRep)" |
|
508 |
where |
|
509 |
"TypeRep_fun1 f = |
|
510 |
alg_defl.basis_fun (\<lambda>a. |
|
511 |
alg_defl_principal ( |
|
512 |
Abs_fin_defl (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)))" |
|
513 |
||
514 |
definition |
|
515 |
TypeRep_fun2 :: |
|
516 |
"((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) |
|
517 |
\<Rightarrow> (TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep)" |
|
518 |
where |
|
519 |
"TypeRep_fun2 f = |
|
520 |
alg_defl.basis_fun (\<lambda>a. |
|
521 |
alg_defl.basis_fun (\<lambda>b. |
|
522 |
alg_defl_principal ( |
|
523 |
Abs_fin_defl (udom_emb oo |
|
524 |
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))" |
|
525 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
526 |
definition "cfun_defl = TypeRep_fun2 cfun_map" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
527 |
definition "ssum_defl = TypeRep_fun2 ssum_map" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
528 |
definition "sprod_defl = TypeRep_fun2 sprod_map" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
529 |
definition "cprod_defl = TypeRep_fun2 cprod_map" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
530 |
definition "u_defl = TypeRep_fun1 u_map" |
33588 | 531 |
|
532 |
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b" |
|
533 |
unfolding below_fin_defl_def . |
|
534 |
||
535 |
lemma cast_TypeRep_fun1: |
|
536 |
assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)" |
|
537 |
shows "cast\<cdot>(TypeRep_fun1 f\<cdot>A) = udom_emb oo f\<cdot>(cast\<cdot>A) oo udom_prj" |
|
538 |
proof - |
|
539 |
have 1: "\<And>a. finite_deflation (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)" |
|
540 |
apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom]) |
|
541 |
apply (rule f, rule finite_deflation_Rep_fin_defl) |
|
542 |
done |
|
543 |
show ?thesis |
|
544 |
by (induct A rule: alg_defl.principal_induct, simp) |
|
545 |
(simp only: TypeRep_fun1_def |
|
546 |
alg_defl.basis_fun_principal |
|
547 |
alg_defl.basis_fun_mono |
|
548 |
alg_defl.principal_mono |
|
549 |
Abs_fin_defl_mono [OF 1 1] |
|
550 |
monofun_cfun below_refl |
|
551 |
Rep_fin_defl_mono |
|
552 |
cast_alg_defl_principal |
|
553 |
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
|
554 |
qed |
|
555 |
||
556 |
lemma cast_TypeRep_fun2: |
|
557 |
assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow> |
|
558 |
finite_deflation (f\<cdot>a\<cdot>b)" |
|
559 |
shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) = udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" |
|
560 |
proof - |
|
561 |
have 1: "\<And>a b. finite_deflation |
|
562 |
(udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)" |
|
563 |
apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom]) |
|
564 |
apply (rule f, (rule finite_deflation_Rep_fin_defl)+) |
|
565 |
done |
|
566 |
show ?thesis |
|
567 |
by (induct A B rule: alg_defl.principal_induct2, simp, simp) |
|
568 |
(simp only: TypeRep_fun2_def |
|
569 |
alg_defl.basis_fun_principal |
|
570 |
alg_defl.basis_fun_mono |
|
571 |
alg_defl.principal_mono |
|
572 |
Abs_fin_defl_mono [OF 1 1] |
|
573 |
monofun_cfun below_refl |
|
574 |
Rep_fin_defl_mono |
|
575 |
cast_alg_defl_principal |
|
576 |
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
|
577 |
qed |
|
578 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
579 |
lemma cast_cfun_defl: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
580 |
"cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
581 |
unfolding cfun_defl_def |
33588 | 582 |
apply (rule cast_TypeRep_fun2) |
583 |
apply (erule (1) finite_deflation_cfun_map) |
|
584 |
done |
|
585 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
586 |
lemma cast_ssum_defl: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
587 |
"cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
588 |
unfolding ssum_defl_def |
33588 | 589 |
apply (rule cast_TypeRep_fun2) |
590 |
apply (erule (1) finite_deflation_ssum_map) |
|
591 |
done |
|
592 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
593 |
lemma cast_sprod_defl: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
594 |
"cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
595 |
unfolding sprod_defl_def |
33588 | 596 |
apply (rule cast_TypeRep_fun2) |
597 |
apply (erule (1) finite_deflation_sprod_map) |
|
598 |
done |
|
599 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
600 |
lemma cast_cprod_defl: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
601 |
"cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
602 |
unfolding cprod_defl_def |
33588 | 603 |
apply (rule cast_TypeRep_fun2) |
604 |
apply (erule (1) finite_deflation_cprod_map) |
|
605 |
done |
|
606 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
607 |
lemma cast_u_defl: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
608 |
"cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
609 |
unfolding u_defl_def |
33588 | 610 |
apply (rule cast_TypeRep_fun1) |
611 |
apply (erule finite_deflation_u_map) |
|
612 |
done |
|
613 |
||
614 |
text {* REP of type constructor = type combinator *} |
|
615 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
616 |
lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)" |
33588 | 617 |
apply (rule cast_eq_imp_eq, rule ext_cfun) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
618 |
apply (simp add: cast_REP cast_cfun_defl) |
33588 | 619 |
apply (simp add: cfun_map_def) |
620 |
apply (simp only: prj_cfun_def emb_cfun_def) |
|
621 |
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom]) |
|
622 |
done |
|
623 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
624 |
lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)" |
33588 | 625 |
apply (rule cast_eq_imp_eq, rule ext_cfun) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
626 |
apply (simp add: cast_REP cast_ssum_defl) |
33588 | 627 |
apply (simp add: prj_ssum_def) |
628 |
apply (simp add: emb_ssum_def) |
|
629 |
apply (simp add: ssum_map_map cfcomp1) |
|
630 |
done |
|
631 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
632 |
lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)" |
33588 | 633 |
apply (rule cast_eq_imp_eq, rule ext_cfun) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
634 |
apply (simp add: cast_REP cast_sprod_defl) |
33588 | 635 |
apply (simp add: prj_sprod_def) |
636 |
apply (simp add: emb_sprod_def) |
|
637 |
apply (simp add: sprod_map_map cfcomp1) |
|
638 |
done |
|
639 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
640 |
lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)" |
33588 | 641 |
apply (rule cast_eq_imp_eq, rule ext_cfun) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
642 |
apply (simp add: cast_REP cast_cprod_defl) |
33588 | 643 |
apply (simp add: prj_cprod_def) |
644 |
apply (simp add: emb_cprod_def) |
|
645 |
apply (simp add: cprod_map_map cfcomp1) |
|
646 |
done |
|
647 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
648 |
lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)" |
33588 | 649 |
apply (rule cast_eq_imp_eq, rule ext_cfun) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
650 |
apply (simp add: cast_REP cast_u_defl) |
33588 | 651 |
apply (simp add: prj_u_def) |
652 |
apply (simp add: emb_u_def) |
|
653 |
apply (simp add: u_map_map cfcomp1) |
|
654 |
done |
|
655 |
||
656 |
lemmas REP_simps = |
|
657 |
REP_cfun |
|
658 |
REP_ssum |
|
659 |
REP_sprod |
|
660 |
REP_cprod |
|
661 |
REP_up |
|
662 |
||
663 |
subsection {* Isomorphic deflations *} |
|
664 |
||
665 |
definition |
|
666 |
isodefl :: "('a::rep \<rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> bool" |
|
667 |
where |
|
668 |
"isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj" |
|
669 |
||
670 |
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t" |
|
671 |
unfolding isodefl_def by (simp add: ext_cfun) |
|
672 |
||
673 |
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))" |
|
674 |
unfolding isodefl_def by (simp add: ext_cfun) |
|
675 |
||
676 |
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>" |
|
677 |
unfolding isodefl_def |
|
678 |
by (drule cfun_fun_cong [where x="\<bottom>"], simp) |
|
679 |
||
680 |
lemma isodefl_imp_deflation: |
|
681 |
fixes d :: "'a::rep \<rightarrow> 'a" |
|
682 |
assumes "isodefl d t" shows "deflation d" |
|
683 |
proof |
|
684 |
note prems [unfolded isodefl_def, simp] |
|
685 |
fix x :: 'a |
|
686 |
show "d\<cdot>(d\<cdot>x) = d\<cdot>x" |
|
687 |
using cast.idem [of t "emb\<cdot>x"] by simp |
|
688 |
show "d\<cdot>x \<sqsubseteq> x" |
|
689 |
using cast.below [of t "emb\<cdot>x"] by simp |
|
690 |
qed |
|
691 |
||
692 |
lemma isodefl_ID_REP: "isodefl (ID :: 'a \<rightarrow> 'a) REP('a)" |
|
693 |
unfolding isodefl_def by (simp add: cast_REP) |
|
694 |
||
695 |
lemma isodefl_REP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) REP('a) \<Longrightarrow> d = ID" |
|
696 |
unfolding isodefl_def |
|
697 |
apply (simp add: cast_REP) |
|
698 |
apply (simp add: expand_cfun_eq) |
|
699 |
apply (rule allI) |
|
700 |
apply (drule_tac x="emb\<cdot>x" in spec) |
|
701 |
apply simp |
|
702 |
done |
|
703 |
||
704 |
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>" |
|
705 |
unfolding isodefl_def by (simp add: expand_cfun_eq) |
|
706 |
||
707 |
lemma adm_isodefl: |
|
708 |
"cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))" |
|
709 |
unfolding isodefl_def by simp |
|
710 |
||
711 |
lemma isodefl_lub: |
|
712 |
assumes "chain d" and "chain t" |
|
713 |
assumes "\<And>i. isodefl (d i) (t i)" |
|
714 |
shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)" |
|
715 |
using prems unfolding isodefl_def |
|
716 |
by (simp add: contlub_cfun_arg contlub_cfun_fun) |
|
717 |
||
718 |
lemma isodefl_fix: |
|
719 |
assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)" |
|
720 |
shows "isodefl (fix\<cdot>f) (fix\<cdot>g)" |
|
721 |
unfolding fix_def2 |
|
722 |
apply (rule isodefl_lub, simp, simp) |
|
723 |
apply (induct_tac i) |
|
724 |
apply (simp add: isodefl_bottom) |
|
725 |
apply (simp add: prems) |
|
726 |
done |
|
727 |
||
728 |
lemma isodefl_coerce: |
|
729 |
fixes d :: "'a \<rightarrow> 'a" |
|
730 |
assumes REP: "REP('b) = REP('a)" |
|
731 |
shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t" |
|
732 |
unfolding isodefl_def |
|
733 |
apply (simp add: expand_cfun_eq) |
|
734 |
apply (simp add: emb_coerce coerce_prj REP) |
|
735 |
done |
|
736 |
||
33779 | 737 |
lemma isodefl_abs_rep: |
738 |
fixes abs and rep and d |
|
739 |
assumes REP: "REP('b) = REP('a)" |
|
740 |
assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)" |
|
741 |
assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)" |
|
742 |
shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t" |
|
743 |
unfolding abs_def rep_def using REP by (rule isodefl_coerce) |
|
744 |
||
33588 | 745 |
lemma isodefl_cfun: |
746 |
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
747 |
isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)" |
33588 | 748 |
apply (rule isodeflI) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
749 |
apply (simp add: cast_cfun_defl cast_isodefl) |
33588 | 750 |
apply (simp add: emb_cfun_def prj_cfun_def) |
751 |
apply (simp add: cfun_map_map cfcomp1) |
|
752 |
done |
|
753 |
||
754 |
lemma isodefl_ssum: |
|
755 |
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
756 |
isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)" |
33588 | 757 |
apply (rule isodeflI) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
758 |
apply (simp add: cast_ssum_defl cast_isodefl) |
33588 | 759 |
apply (simp add: emb_ssum_def prj_ssum_def) |
760 |
apply (simp add: ssum_map_map isodefl_strict) |
|
761 |
done |
|
762 |
||
763 |
lemma isodefl_sprod: |
|
764 |
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
765 |
isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)" |
33588 | 766 |
apply (rule isodeflI) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
767 |
apply (simp add: cast_sprod_defl cast_isodefl) |
33588 | 768 |
apply (simp add: emb_sprod_def prj_sprod_def) |
769 |
apply (simp add: sprod_map_map isodefl_strict) |
|
770 |
done |
|
771 |
||
33786 | 772 |
lemma isodefl_cprod: |
773 |
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow> |
|
774 |
isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)" |
|
775 |
apply (rule isodeflI) |
|
776 |
apply (simp add: cast_cprod_defl cast_isodefl) |
|
777 |
apply (simp add: emb_cprod_def prj_cprod_def) |
|
778 |
apply (simp add: cprod_map_map cfcomp1) |
|
779 |
done |
|
780 |
||
33588 | 781 |
lemma isodefl_u: |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
782 |
"isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)" |
33588 | 783 |
apply (rule isodeflI) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33779
diff
changeset
|
784 |
apply (simp add: cast_u_defl cast_isodefl) |
33588 | 785 |
apply (simp add: emb_u_def prj_u_def) |
786 |
apply (simp add: u_map_map) |
|
787 |
done |
|
788 |
||
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
789 |
subsection {* Constructing Domain Isomorphisms *} |
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
790 |
|
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
791 |
use "Tools/Domain/domain_isomorphism.ML" |
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
792 |
|
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
793 |
setup {* |
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
794 |
fold Domain_Isomorphism.add_type_constructor |
35525 | 795 |
[(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun}, |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
796 |
@{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}), |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
797 |
|
35525 | 798 |
(@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum}, |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
799 |
@{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}), |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
800 |
|
35525 | 801 |
(@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod}, |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
802 |
@{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}), |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
803 |
|
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
804 |
(@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod}, |
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
805 |
@{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}), |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
806 |
|
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
807 |
(@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up}, |
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35475
diff
changeset
|
808 |
@{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})] |
33794
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
809 |
*} |
364bc92ba081
set up domain_isomorphism package in Representable.thy
huffman
parents:
33786
diff
changeset
|
810 |
|
33588 | 811 |
end |