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