author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58880 | 0baae4311a9f |
child 61169 | 4de9ff3ea29a |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Representable.thy |
25903 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
58880 | 5 |
section {* Representable domains *} |
25903 | 6 |
|
41285 | 7 |
theory Representable |
44781 | 8 |
imports Algebraic Map_Functions "~~/src/HOL/Library/Countable" |
25903 | 9 |
begin |
10 |
||
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
11 |
default_sort cpo |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
12 |
|
41285 | 13 |
subsection {* Class of representable domains *} |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
14 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
15 |
text {* |
40497 | 16 |
We define a ``domain'' as a pcpo that is isomorphic to some |
17 |
algebraic deflation over the universal domain; this is equivalent |
|
18 |
to being omega-bifinite. |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
19 |
|
40497 | 20 |
A predomain is a cpo that, when lifted, becomes a domain. |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
21 |
Predomains are represented by deflations over a lifted universal |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
22 |
domain type. |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
23 |
*} |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
24 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
25 |
class predomain_syn = cpo + |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
26 |
fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
27 |
fixes liftprj :: "udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
28 |
fixes liftdefl :: "'a itself \<Rightarrow> udom u defl" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
29 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
30 |
class predomain = predomain_syn + |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
31 |
assumes predomain_ep: "ep_pair liftemb liftprj" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
32 |
assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
33 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
34 |
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))") |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
35 |
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
36 |
|
41436 | 37 |
definition liftdefl_of :: "udom defl \<rightarrow> udom u defl" |
38 |
where "liftdefl_of = defl_fun1 ID ID u_map" |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
39 |
|
41436 | 40 |
lemma cast_liftdefl_of: "cast\<cdot>(liftdefl_of\<cdot>t) = u_map\<cdot>(cast\<cdot>t)" |
41 |
by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map) |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
42 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
43 |
class "domain" = predomain_syn + pcpo + |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
44 |
fixes emb :: "'a \<rightarrow> udom" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
45 |
fixes prj :: "udom \<rightarrow> 'a" |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
46 |
fixes defl :: "'a itself \<Rightarrow> udom defl" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
47 |
assumes ep_pair_emb_prj: "ep_pair emb prj" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
48 |
assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
49 |
assumes liftemb_eq: "liftemb = u_map\<cdot>emb" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
50 |
assumes liftprj_eq: "liftprj = u_map\<cdot>prj" |
41436 | 51 |
assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))" |
31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset
|
52 |
|
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
53 |
syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))") |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
54 |
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
55 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
56 |
instance "domain" \<subseteq> predomain |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
57 |
proof |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
58 |
show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
59 |
unfolding liftemb_eq liftprj_eq |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
60 |
by (intro ep_pair_u_map ep_pair_emb_prj) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
61 |
show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
62 |
unfolding liftemb_eq liftprj_eq liftdefl_eq |
41436 | 63 |
by (simp add: cast_liftdefl_of cast_DEFL u_map_oo) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
64 |
qed |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
65 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
66 |
text {* |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
67 |
Constants @{const liftemb} and @{const liftprj} imply class predomain. |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
68 |
*} |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
69 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
70 |
setup {* |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
71 |
fold Sign.add_const_constraint |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
72 |
[(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}), |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
73 |
(@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}), |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
74 |
(@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})] |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
75 |
*} |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
76 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
77 |
interpretation predomain: pcpo_ep_pair liftemb liftprj |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
78 |
unfolding pcpo_ep_pair_def by (rule predomain_ep) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
79 |
|
40497 | 80 |
interpretation "domain": pcpo_ep_pair emb prj |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
81 |
unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
82 |
|
40497 | 83 |
lemmas emb_inverse = domain.e_inverse |
84 |
lemmas emb_prj_below = domain.e_p_below |
|
85 |
lemmas emb_eq_iff = domain.e_eq_iff |
|
86 |
lemmas emb_strict = domain.e_strict |
|
87 |
lemmas prj_strict = domain.p_strict |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
88 |
|
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
89 |
subsection {* Domains are bifinite *} |
33587 | 90 |
|
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
91 |
lemma approx_chain_ep_cast: |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
92 |
assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)" |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
93 |
assumes cast_t: "cast\<cdot>t = e oo p" |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
94 |
shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
95 |
proof - |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
96 |
interpret ep_pair e p by fact |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
97 |
obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
98 |
and t: "t = (\<Squnion>i. defl_principal (Y i))" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
99 |
by (rule defl.obtain_principal_chain) |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
100 |
def approx \<equiv> "\<lambda>i. (p oo cast\<cdot>(defl_principal (Y i)) oo e) :: 'a \<rightarrow> 'a" |
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
101 |
have "approx_chain approx" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
102 |
proof (rule approx_chain.intro) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
103 |
show "chain (\<lambda>i. approx i)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
104 |
unfolding approx_def by (simp add: Y) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
105 |
show "(\<Squnion>i. approx i) = ID" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
106 |
unfolding approx_def |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
107 |
by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
108 |
show "\<And>i. finite_deflation (approx i)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
109 |
unfolding approx_def |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
110 |
apply (rule finite_deflation_p_d_e) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
111 |
apply (rule finite_deflation_cast) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
112 |
apply (rule defl.compact_principal) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
113 |
apply (rule below_trans [OF monofun_cfun_fun]) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
114 |
apply (rule is_ub_thelub, simp add: Y) |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
115 |
apply (simp add: lub_distribs Y t [symmetric] cast_t) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
116 |
done |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
117 |
qed |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
118 |
thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
119 |
qed |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
120 |
|
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
121 |
instance "domain" \<subseteq> bifinite |
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
122 |
by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL]) |
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
123 |
|
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
124 |
instance predomain \<subseteq> profinite |
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
125 |
by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl]) |
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
126 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
127 |
subsection {* Universal domain ep-pairs *} |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
128 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
129 |
definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
130 |
definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))" |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
131 |
|
41297 | 132 |
definition "prod_emb = udom_emb (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
133 |
definition "prod_prj = udom_prj (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
|
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
134 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
135 |
definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
136 |
definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
137 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
138 |
definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
139 |
definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
140 |
|
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
141 |
definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
142 |
definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
143 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
144 |
lemma ep_pair_u: "ep_pair u_emb u_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
145 |
unfolding u_emb_def u_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
146 |
by (simp add: ep_pair_udom approx_chain_u_map) |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
147 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
148 |
lemma ep_pair_prod: "ep_pair prod_emb prod_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
149 |
unfolding prod_emb_def prod_prj_def |
41297 | 150 |
by (simp add: ep_pair_udom approx_chain_prod_map) |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
151 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
152 |
lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
153 |
unfolding sprod_emb_def sprod_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
154 |
by (simp add: ep_pair_udom approx_chain_sprod_map) |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
155 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
156 |
lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
157 |
unfolding ssum_emb_def ssum_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
158 |
by (simp add: ep_pair_udom approx_chain_ssum_map) |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
159 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
160 |
lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
161 |
unfolding sfun_emb_def sfun_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
162 |
by (simp add: ep_pair_udom approx_chain_sfun_map) |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
163 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
164 |
subsection {* Type combinators *} |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
165 |
|
41437 | 166 |
definition u_defl :: "udom defl \<rightarrow> udom defl" |
167 |
where "u_defl = defl_fun1 u_emb u_prj u_map" |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
168 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
169 |
definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" |
41297 | 170 |
where "prod_defl = defl_fun2 prod_emb prod_prj prod_map" |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
171 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
172 |
definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
173 |
where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map" |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
174 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
175 |
definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
176 |
where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map" |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
177 |
|
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
178 |
definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
179 |
where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map" |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
180 |
|
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
181 |
lemma cast_u_defl: |
41437 | 182 |
"cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj" |
183 |
using ep_pair_u finite_deflation_u_map |
|
184 |
unfolding u_defl_def by (rule cast_defl_fun1) |
|
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
185 |
|
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
186 |
lemma cast_prod_defl: |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
187 |
"cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = |
41297 | 188 |
prod_emb oo prod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj" |
189 |
using ep_pair_prod finite_deflation_prod_map |
|
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
190 |
unfolding prod_defl_def by (rule cast_defl_fun2) |
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
191 |
|
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
192 |
lemma cast_sprod_defl: |
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
193 |
"cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
194 |
sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
195 |
using ep_pair_sprod finite_deflation_sprod_map |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
196 |
unfolding sprod_defl_def by (rule cast_defl_fun2) |
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
197 |
|
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
198 |
lemma cast_ssum_defl: |
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
199 |
"cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
200 |
ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
201 |
using ep_pair_ssum finite_deflation_ssum_map |
40484
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
202 |
unfolding ssum_defl_def by (rule cast_defl_fun2) |
768f7e264e2b
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents:
40086
diff
changeset
|
203 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
204 |
lemma cast_sfun_defl: |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
205 |
"cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) = |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
206 |
sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
207 |
using ep_pair_sfun finite_deflation_sfun_map |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
208 |
unfolding sfun_defl_def by (rule cast_defl_fun2) |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
209 |
|
41437 | 210 |
text {* Special deflation combinator for unpointed types. *} |
211 |
||
212 |
definition u_liftdefl :: "udom u defl \<rightarrow> udom defl" |
|
213 |
where "u_liftdefl = defl_fun1 u_emb u_prj ID" |
|
214 |
||
215 |
lemma cast_u_liftdefl: |
|
216 |
"cast\<cdot>(u_liftdefl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj" |
|
217 |
unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u) |
|
218 |
||
219 |
lemma u_liftdefl_liftdefl_of: |
|
220 |
"u_liftdefl\<cdot>(liftdefl_of\<cdot>A) = u_defl\<cdot>A" |
|
221 |
by (rule cast_eq_imp_eq) |
|
222 |
(simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl) |
|
223 |
||
40506 | 224 |
subsection {* Class instance proofs *} |
225 |
||
226 |
subsubsection {* Universal domain *} |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
227 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
228 |
instantiation udom :: "domain" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
229 |
begin |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
230 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
231 |
definition [simp]: |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
232 |
"emb = (ID :: udom \<rightarrow> udom)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
233 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
234 |
definition [simp]: |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
235 |
"prj = (ID :: udom \<rightarrow> udom)" |
25903 | 236 |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
237 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
238 |
"defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))" |
33808 | 239 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
240 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
241 |
"(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
242 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
243 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
244 |
"(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
245 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
246 |
definition |
41436 | 247 |
"liftdefl (t::udom itself) = liftdefl_of\<cdot>DEFL(udom)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
248 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
249 |
instance proof |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
250 |
show "ep_pair emb (prj :: udom \<rightarrow> udom)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
251 |
by (simp add: ep_pair.intro) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
252 |
show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
253 |
unfolding defl_udom_def |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
254 |
apply (subst contlub_cfun_arg) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
255 |
apply (rule chainI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
256 |
apply (rule defl.principal_mono) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
257 |
apply (simp add: below_fin_defl_def) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
258 |
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
259 |
apply (rule chainE) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
260 |
apply (rule chain_udom_approx) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
261 |
apply (subst cast_defl_principal) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
262 |
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
263 |
done |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
264 |
qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+ |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
265 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
266 |
end |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
267 |
|
40506 | 268 |
subsubsection {* Lifted cpo *} |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
269 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
270 |
instantiation u :: (predomain) "domain" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
271 |
begin |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
272 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
273 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
274 |
"emb = u_emb oo liftemb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
275 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
276 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
277 |
"prj = liftprj oo u_prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
278 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
279 |
definition |
41437 | 280 |
"defl (t::'a u itself) = u_liftdefl\<cdot>LIFTDEFL('a)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
281 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
282 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
283 |
"(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
284 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
285 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
286 |
"(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
287 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
288 |
definition |
41436 | 289 |
"liftdefl (t::'a u itself) = liftdefl_of\<cdot>DEFL('a u)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
290 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
291 |
instance proof |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
292 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a u)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
293 |
unfolding emb_u_def prj_u_def |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
294 |
by (intro ep_pair_comp ep_pair_u predomain_ep) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
295 |
show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
296 |
unfolding emb_u_def prj_u_def defl_u_def |
41437 | 297 |
by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
298 |
qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+ |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
299 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
300 |
end |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
301 |
|
41437 | 302 |
lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
303 |
by (rule defl_u_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
304 |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
305 |
subsubsection {* Strict function space *} |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
306 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
307 |
instantiation sfun :: ("domain", "domain") "domain" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
308 |
begin |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
309 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
310 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
311 |
"emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb" |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
312 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
313 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
314 |
"prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj" |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
315 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
316 |
definition |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
317 |
"defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
318 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
319 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
320 |
"(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
321 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
322 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
323 |
"(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj" |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
324 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
325 |
definition |
41436 | 326 |
"liftdefl (t::('a \<rightarrow>! 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow>! 'b)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
327 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
328 |
instance proof |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
329 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
330 |
unfolding emb_sfun_def prj_sfun_def |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
331 |
by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
332 |
show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
333 |
unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
334 |
by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
335 |
qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+ |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
336 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
337 |
end |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
338 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
339 |
lemma DEFL_sfun: |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
340 |
"DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
341 |
by (rule defl_sfun_def) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
342 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
343 |
subsubsection {* Continuous function space *} |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
344 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
345 |
instantiation cfun :: (predomain, "domain") "domain" |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
346 |
begin |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
347 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
348 |
definition |
40830 | 349 |
"emb = emb oo encode_cfun" |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
350 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
351 |
definition |
40830 | 352 |
"prj = decode_cfun oo prj" |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
353 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
354 |
definition |
40830 | 355 |
"defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
356 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
357 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
358 |
"(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
359 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
360 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
361 |
"(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
362 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
363 |
definition |
41436 | 364 |
"liftdefl (t::('a \<rightarrow> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow> 'b)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
365 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
366 |
instance proof |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
367 |
have "ep_pair encode_cfun decode_cfun" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
368 |
by (rule ep_pair.intro, simp_all) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40506
diff
changeset
|
369 |
thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
370 |
unfolding emb_cfun_def prj_cfun_def |
40830 | 371 |
using ep_pair_emb_prj by (rule ep_pair_comp) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
372 |
show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
40830 | 373 |
unfolding emb_cfun_def prj_cfun_def defl_cfun_def |
374 |
by (simp add: cast_DEFL cfcomp1) |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
375 |
qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+ |
25903 | 376 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
377 |
end |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
378 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
379 |
lemma DEFL_cfun: |
40830 | 380 |
"DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
381 |
by (rule defl_cfun_def) |
39972
4244ff4f9649
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
Brian Huffman <brianh@cs.pdx.edu>
parents:
37678
diff
changeset
|
382 |
|
40506 | 383 |
subsubsection {* Strict product *} |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
384 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
385 |
instantiation sprod :: ("domain", "domain") "domain" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
386 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
387 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
388 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
389 |
"emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
390 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
391 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
392 |
"prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
393 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
394 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
395 |
"defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
396 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
397 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
398 |
"(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
399 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
400 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
401 |
"(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
402 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
403 |
definition |
41436 | 404 |
"liftdefl (t::('a \<otimes> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<otimes> 'b)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
405 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
406 |
instance proof |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
407 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
408 |
unfolding emb_sprod_def prj_sprod_def |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
409 |
by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
410 |
show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
411 |
unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
412 |
by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
413 |
qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+ |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
414 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
415 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
416 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
417 |
lemma DEFL_sprod: |
40497 | 418 |
"DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
419 |
by (rule defl_sprod_def) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
420 |
|
40830 | 421 |
subsubsection {* Cartesian product *} |
422 |
||
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
423 |
definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
424 |
where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
425 |
(encode_prod_u oo u_map\<cdot>prod_prj) sprod_map" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
426 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
427 |
lemma cast_prod_liftdefl: |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
428 |
"cast\<cdot>(prod_liftdefl\<cdot>a\<cdot>b) = |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
429 |
(u_map\<cdot>prod_emb oo decode_prod_u) oo sprod_map\<cdot>(cast\<cdot>a)\<cdot>(cast\<cdot>b) oo |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
430 |
(encode_prod_u oo u_map\<cdot>prod_prj)" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
431 |
unfolding prod_liftdefl_def |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
432 |
apply (rule cast_defl_fun2) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
433 |
apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
434 |
apply (simp add: ep_pair.intro) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
435 |
apply (erule (1) finite_deflation_sprod_map) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
436 |
done |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
437 |
|
40830 | 438 |
instantiation prod :: (predomain, predomain) predomain |
439 |
begin |
|
440 |
||
441 |
definition |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
442 |
"liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
443 |
(sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)" |
40830 | 444 |
|
445 |
definition |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
446 |
"liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
447 |
(encode_prod_u oo u_map\<cdot>prod_prj)" |
40830 | 448 |
|
449 |
definition |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
450 |
"liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" |
40830 | 451 |
|
452 |
instance proof |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
453 |
show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)" |
40830 | 454 |
unfolding liftemb_prod_def liftprj_prod_def |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
455 |
by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
456 |
ep_pair_prod predomain_ep, simp_all add: ep_pair.intro) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
457 |
show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)" |
40830 | 458 |
unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
459 |
by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map) |
40830 | 460 |
qed |
461 |
||
462 |
end |
|
463 |
||
464 |
instantiation prod :: ("domain", "domain") "domain" |
|
465 |
begin |
|
466 |
||
467 |
definition |
|
41297 | 468 |
"emb = prod_emb oo prod_map\<cdot>emb\<cdot>emb" |
40830 | 469 |
|
470 |
definition |
|
41297 | 471 |
"prj = prod_map\<cdot>prj\<cdot>prj oo prod_prj" |
40830 | 472 |
|
473 |
definition |
|
474 |
"defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
|
475 |
||
476 |
instance proof |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
477 |
show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)" |
40830 | 478 |
unfolding emb_prod_def prj_prod_def |
41297 | 479 |
by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
480 |
show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)" |
40830 | 481 |
unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl |
41297 | 482 |
by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
483 |
show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
484 |
unfolding emb_prod_def liftemb_prod_def liftemb_eq |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
485 |
unfolding encode_prod_u_def decode_prod_u_def |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
486 |
by (rule cfun_eqI, case_tac x, simp, clarsimp) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
487 |
show 4: "liftprj = u_map\<cdot>(prj :: udom \<rightarrow> 'a \<times> 'b)" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
488 |
unfolding prj_prod_def liftprj_prod_def liftprj_eq |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
489 |
unfolding encode_prod_u_def decode_prod_u_def |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
490 |
apply (rule cfun_eqI, case_tac x, simp) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
491 |
apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
492 |
done |
41436 | 493 |
show 5: "LIFTDEFL('a \<times> 'b) = liftdefl_of\<cdot>DEFL('a \<times> 'b)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
494 |
by (rule cast_eq_imp_eq) |
41436 | 495 |
(simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo) |
40830 | 496 |
qed |
497 |
||
498 |
end |
|
499 |
||
500 |
lemma DEFL_prod: |
|
501 |
"DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
|
502 |
by (rule defl_prod_def) |
|
503 |
||
504 |
lemma LIFTDEFL_prod: |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
505 |
"LIFTDEFL('a::predomain \<times> 'b::predomain) = |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
506 |
prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" |
40830 | 507 |
by (rule liftdefl_prod_def) |
508 |
||
41034 | 509 |
subsubsection {* Unit type *} |
510 |
||
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
511 |
instantiation unit :: "domain" |
41034 | 512 |
begin |
513 |
||
514 |
definition |
|
515 |
"emb = (\<bottom> :: unit \<rightarrow> udom)" |
|
516 |
||
517 |
definition |
|
518 |
"prj = (\<bottom> :: udom \<rightarrow> unit)" |
|
519 |
||
520 |
definition |
|
521 |
"defl (t::unit itself) = \<bottom>" |
|
522 |
||
523 |
definition |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
524 |
"(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb" |
41034 | 525 |
|
526 |
definition |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
527 |
"(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj" |
41034 | 528 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
529 |
definition |
41436 | 530 |
"liftdefl (t::unit itself) = liftdefl_of\<cdot>DEFL(unit)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
531 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
532 |
instance proof |
41034 | 533 |
show "ep_pair emb (prj :: udom \<rightarrow> unit)" |
534 |
unfolding emb_unit_def prj_unit_def |
|
535 |
by (simp add: ep_pair.intro) |
|
536 |
show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)" |
|
537 |
unfolding emb_unit_def prj_unit_def defl_unit_def by simp |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
538 |
qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+ |
41034 | 539 |
|
540 |
end |
|
541 |
||
40506 | 542 |
subsubsection {* Discrete cpo *} |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
543 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
544 |
instantiation discr :: (countable) predomain |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
545 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
546 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
547 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
548 |
"(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
549 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
550 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
551 |
"(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
552 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
553 |
definition |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
554 |
"liftdefl (t::'a discr itself) = |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
555 |
(\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
556 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
557 |
instance proof |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
558 |
show 1: "ep_pair liftemb (liftprj :: udom u \<rightarrow> 'a discr u)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
559 |
unfolding liftemb_discr_def liftprj_discr_def |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
560 |
apply (intro ep_pair_comp ep_pair_udom [OF discr_approx]) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
561 |
apply (rule ep_pair.intro) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
562 |
apply (simp add: strictify_conv_if) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
563 |
apply (case_tac y, simp, simp add: strictify_conv_if) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
564 |
done |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
565 |
show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \<rightarrow> 'a discr u)" |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
566 |
unfolding liftdefl_discr_def |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
567 |
apply (subst contlub_cfun_arg) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
568 |
apply (rule chainI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
569 |
apply (rule defl.principal_mono) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
570 |
apply (simp add: below_fin_defl_def) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
571 |
apply (simp add: Abs_fin_defl_inverse |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
572 |
ep_pair.finite_deflation_e_d_p [OF 1] |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
573 |
approx_chain.finite_deflation_approx [OF discr_approx]) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
574 |
apply (intro monofun_cfun below_refl) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
575 |
apply (rule chainE) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
576 |
apply (rule chain_discr_approx) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
577 |
apply (subst cast_defl_principal) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
578 |
apply (simp add: Abs_fin_defl_inverse |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
579 |
ep_pair.finite_deflation_e_d_p [OF 1] |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
580 |
approx_chain.finite_deflation_approx [OF discr_approx]) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
581 |
apply (simp add: lub_distribs) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
582 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
583 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
584 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
585 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
586 |
|
40506 | 587 |
subsubsection {* Strict sum *} |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
588 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
589 |
instantiation ssum :: ("domain", "domain") "domain" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
590 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
591 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
592 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
593 |
"emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
594 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
595 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
596 |
"prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
597 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
598 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
599 |
"defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
600 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
601 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
602 |
"(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
603 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
604 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
605 |
"(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
606 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
607 |
definition |
41436 | 608 |
"liftdefl (t::('a \<oplus> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<oplus> 'b)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
609 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
610 |
instance proof |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
611 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
612 |
unfolding emb_ssum_def prj_ssum_def |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41287
diff
changeset
|
613 |
by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
614 |
show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
615 |
unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
616 |
by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
617 |
qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+ |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
618 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
619 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
620 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
621 |
lemma DEFL_ssum: |
40497 | 622 |
"DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
623 |
by (rule defl_ssum_def) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
624 |
|
40506 | 625 |
subsubsection {* Lifted HOL type *} |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
626 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
627 |
instantiation lift :: (countable) "domain" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
628 |
begin |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
629 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
630 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
631 |
"emb = emb oo (\<Lambda> x. Rep_lift x)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
632 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
633 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
634 |
"prj = (\<Lambda> y. Abs_lift y) oo prj" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
635 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
636 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
637 |
"defl (t::'a lift itself) = DEFL('a discr u)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
638 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
639 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
640 |
"(liftemb :: 'a lift u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
641 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
642 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
643 |
"(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
644 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
645 |
definition |
41436 | 646 |
"liftdefl (t::'a lift itself) = liftdefl_of\<cdot>DEFL('a lift)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
647 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
648 |
instance proof |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
649 |
note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
650 |
have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
651 |
by (simp add: ep_pair_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
652 |
thus "ep_pair emb (prj :: udom \<rightarrow> 'a lift)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
653 |
unfolding emb_lift_def prj_lift_def |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
654 |
using ep_pair_emb_prj by (rule ep_pair_comp) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
655 |
show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
656 |
unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
657 |
by (simp add: cfcomp1) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
658 |
qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+ |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
659 |
|
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
660 |
end |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
661 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40484
diff
changeset
|
662 |
end |