author | huffman |
Sun, 19 Dec 2010 06:59:01 -0800 | |
changeset 41289 | f655912ac235 |
parent 40774 | 0437dbc127b3 |
child 41290 | e9c9577d88b5 |
permissions | -rw-r--r-- |
35473 | 1 |
(* Title: HOLCF/Powerdomains.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Powerdomains *} |
|
6 |
||
7 |
theory Powerdomains |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39973
diff
changeset
|
8 |
imports ConvexPD Domain |
35473 | 9 |
begin |
10 |
||
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
11 |
subsection {* Universal domain embeddings *} |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
12 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
13 |
definition upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
14 |
where "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
15 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
16 |
definition lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
17 |
where "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
18 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
19 |
definition convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
20 |
where "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
21 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
22 |
lemma upper_approx: "approx_chain upper_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
23 |
using upper_map_ID finite_deflation_upper_map |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
24 |
unfolding upper_approx_def by (rule approx_chain_lemma1) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
25 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
26 |
lemma lower_approx: "approx_chain lower_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
27 |
using lower_map_ID finite_deflation_lower_map |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
28 |
unfolding lower_approx_def by (rule approx_chain_lemma1) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
29 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
30 |
lemma convex_approx: "approx_chain convex_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
31 |
using convex_map_ID finite_deflation_convex_map |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
32 |
unfolding convex_approx_def by (rule approx_chain_lemma1) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
33 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
34 |
subsection {* Deflation combinators *} |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
35 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
36 |
definition upper_defl :: "udom defl \<rightarrow> udom defl" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
37 |
where "upper_defl = defl_fun1 upper_approx upper_map" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
38 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
39 |
definition lower_defl :: "udom defl \<rightarrow> udom defl" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
40 |
where "lower_defl = defl_fun1 lower_approx lower_map" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
41 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
42 |
definition convex_defl :: "udom defl \<rightarrow> udom defl" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
43 |
where "convex_defl = defl_fun1 convex_approx convex_map" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
44 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
45 |
lemma cast_upper_defl: |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
46 |
"cast\<cdot>(upper_defl\<cdot>A) = |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
47 |
udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
48 |
using upper_approx finite_deflation_upper_map |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
49 |
unfolding upper_defl_def by (rule cast_defl_fun1) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
50 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
51 |
lemma cast_lower_defl: |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
52 |
"cast\<cdot>(lower_defl\<cdot>A) = |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
53 |
udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
54 |
using lower_approx finite_deflation_lower_map |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
55 |
unfolding lower_defl_def by (rule cast_defl_fun1) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
56 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
57 |
lemma cast_convex_defl: |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
58 |
"cast\<cdot>(convex_defl\<cdot>A) = |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
59 |
udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
60 |
using convex_approx finite_deflation_convex_map |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
61 |
unfolding convex_defl_def by (rule cast_defl_fun1) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
62 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
63 |
subsection {* Domain class instances *} |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
64 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
65 |
instantiation upper_pd :: ("domain") liftdomain |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
66 |
begin |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
67 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
68 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
69 |
"emb = udom_emb upper_approx oo upper_map\<cdot>emb" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
70 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
71 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
72 |
"prj = upper_map\<cdot>prj oo udom_prj upper_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
73 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
74 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
75 |
"defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
76 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
77 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
78 |
"(liftemb :: 'a upper_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
79 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
80 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
81 |
"(liftprj :: udom \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj oo udom_prj u_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
82 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
83 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
84 |
"liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
85 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
86 |
instance |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
87 |
using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
88 |
proof (rule liftdomain_class_intro) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
89 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
90 |
unfolding emb_upper_pd_def prj_upper_pd_def |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
91 |
using ep_pair_udom [OF upper_approx] |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
92 |
by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
93 |
next |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
94 |
show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
95 |
unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
96 |
by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
97 |
qed |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
98 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
99 |
end |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
100 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
101 |
instantiation lower_pd :: ("domain") liftdomain |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
102 |
begin |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
103 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
104 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
105 |
"emb = udom_emb lower_approx oo lower_map\<cdot>emb" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
106 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
107 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
108 |
"prj = lower_map\<cdot>prj oo udom_prj lower_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
109 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
110 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
111 |
"defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
112 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
113 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
114 |
"(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
115 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
116 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
117 |
"(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
118 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
119 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
120 |
"liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
121 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
122 |
instance |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
123 |
using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
124 |
proof (rule liftdomain_class_intro) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
125 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
126 |
unfolding emb_lower_pd_def prj_lower_pd_def |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
127 |
using ep_pair_udom [OF lower_approx] |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
128 |
by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
129 |
next |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
130 |
show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
131 |
unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
132 |
by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
133 |
qed |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
134 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
135 |
end |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
136 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
137 |
instantiation convex_pd :: ("domain") liftdomain |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
138 |
begin |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
139 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
140 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
141 |
"emb = udom_emb convex_approx oo convex_map\<cdot>emb" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
142 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
143 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
144 |
"prj = convex_map\<cdot>prj oo udom_prj convex_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
145 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
146 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
147 |
"defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
148 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
149 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
150 |
"(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
151 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
152 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
153 |
"(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
154 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
155 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
156 |
"liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
157 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
158 |
instance |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
159 |
using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
160 |
proof (rule liftdomain_class_intro) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
161 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
162 |
unfolding emb_convex_pd_def prj_convex_pd_def |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
163 |
using ep_pair_udom [OF convex_approx] |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
164 |
by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
165 |
next |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
166 |
show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
167 |
unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
168 |
by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
169 |
qed |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
170 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
171 |
end |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
172 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
173 |
lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
174 |
by (rule defl_upper_pd_def) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
175 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
176 |
lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
177 |
by (rule defl_lower_pd_def) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
178 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
179 |
lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)" |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
180 |
by (rule defl_convex_pd_def) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
181 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
182 |
subsection {* Isomorphic deflations *} |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
183 |
|
35473 | 184 |
lemma isodefl_upper: |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
185 |
"isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" |
35473 | 186 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
187 |
apply (simp add: cast_upper_defl cast_isodefl) |
35473 | 188 |
apply (simp add: emb_upper_pd_def prj_upper_pd_def) |
189 |
apply (simp add: upper_map_map) |
|
190 |
done |
|
191 |
||
192 |
lemma isodefl_lower: |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
193 |
"isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)" |
35473 | 194 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
195 |
apply (simp add: cast_lower_defl cast_isodefl) |
35473 | 196 |
apply (simp add: emb_lower_pd_def prj_lower_pd_def) |
197 |
apply (simp add: lower_map_map) |
|
198 |
done |
|
199 |
||
200 |
lemma isodefl_convex: |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
201 |
"isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)" |
35473 | 202 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
203 |
apply (simp add: cast_convex_defl cast_isodefl) |
35473 | 204 |
apply (simp add: emb_convex_pd_def prj_convex_pd_def) |
205 |
apply (simp add: convex_map_map) |
|
206 |
done |
|
207 |
||
208 |
subsection {* Domain package setup for powerdomains *} |
|
209 |
||
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
210 |
lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
211 |
lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
212 |
lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
213 |
|
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
214 |
lemmas [domain_deflation] = |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
215 |
deflation_upper_map deflation_lower_map deflation_convex_map |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
216 |
|
35473 | 217 |
setup {* |
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
218 |
fold Domain_Take_Proofs.add_rec_type |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
219 |
[(@{type_name "upper_pd"}, [true]), |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
220 |
(@{type_name "lower_pd"}, [true]), |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
221 |
(@{type_name "convex_pd"}, [true])] |
35473 | 222 |
*} |
223 |
||
224 |
end |