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