author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58880 | 0baae4311a9f |
child 62175 | 8ffc4d0e652d |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Powerdomains.thy |
35473 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
58880 | 5 |
section {* Powerdomains *} |
35473 | 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 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
13 |
definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
14 |
definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
15 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
16 |
definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
17 |
definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
18 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
19 |
definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
20 |
definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
21 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
22 |
lemma ep_pair_upper: "ep_pair upper_emb upper_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
23 |
unfolding upper_emb_def upper_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
24 |
by (simp add: ep_pair_udom approx_chain_upper_map) |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
25 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
26 |
lemma ep_pair_lower: "ep_pair lower_emb lower_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
27 |
unfolding lower_emb_def lower_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
28 |
by (simp add: ep_pair_udom approx_chain_lower_map) |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
29 |
|
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
30 |
lemma ep_pair_convex: "ep_pair convex_emb convex_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
31 |
unfolding convex_emb_def convex_prj_def |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
32 |
by (simp add: ep_pair_udom approx_chain_convex_map) |
41289
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" |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
37 |
where "upper_defl = defl_fun1 upper_emb upper_prj upper_map" |
41289
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" |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
40 |
where "lower_defl = defl_fun1 lower_emb lower_prj lower_map" |
41289
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" |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
43 |
where "convex_defl = defl_fun1 convex_emb convex_prj convex_map" |
41289
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: |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
46 |
"cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
47 |
using ep_pair_upper finite_deflation_upper_map |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
48 |
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
|
49 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
50 |
lemma cast_lower_defl: |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
51 |
"cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
52 |
using ep_pair_lower finite_deflation_lower_map |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
53 |
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
|
54 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
55 |
lemma cast_convex_defl: |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
56 |
"cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj" |
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
57 |
using ep_pair_convex finite_deflation_convex_map |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
58 |
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
|
59 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
60 |
subsection {* Domain class instances *} |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
61 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
62 |
instantiation upper_pd :: ("domain") "domain" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
63 |
begin |
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 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
66 |
"emb = upper_emb oo upper_map\<cdot>emb" |
41289
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 |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
69 |
"prj = upper_map\<cdot>prj oo upper_prj" |
41289
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 |
"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
|
73 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
74 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
75 |
"(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb" |
41289
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 |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
78 |
"(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
79 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
80 |
definition |
41436 | 81 |
"liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
82 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
83 |
instance proof |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
84 |
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
|
85 |
unfolding emb_upper_pd_def prj_upper_pd_def |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
86 |
by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj) |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
87 |
next |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
91 |
qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+ |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
92 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
93 |
end |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
94 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
95 |
instantiation lower_pd :: ("domain") "domain" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
96 |
begin |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
97 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
98 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
99 |
"emb = lower_emb oo lower_map\<cdot>emb" |
41289
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 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
102 |
"prj = lower_map\<cdot>prj oo lower_prj" |
41289
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 |
"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
|
106 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
107 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
108 |
"(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb" |
41289
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 |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
111 |
"(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
112 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
113 |
definition |
41436 | 114 |
"liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
115 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
116 |
instance proof |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
117 |
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
|
118 |
unfolding emb_lower_pd_def prj_lower_pd_def |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
119 |
by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj) |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
120 |
next |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
121 |
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
|
122 |
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
|
123 |
by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
124 |
qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+ |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
125 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
126 |
end |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
127 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
128 |
instantiation convex_pd :: ("domain") "domain" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
129 |
begin |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
130 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
131 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
132 |
"emb = convex_emb oo convex_map\<cdot>emb" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
133 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
134 |
definition |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
135 |
"prj = convex_map\<cdot>prj oo convex_prj" |
41289
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 |
definition |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
138 |
"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
|
139 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
140 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
141 |
"(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb" |
41289
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 |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
144 |
"(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj" |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
145 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
146 |
definition |
41436 | 147 |
"liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
148 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
149 |
instance proof |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
150 |
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
|
151 |
unfolding emb_convex_pd_def prj_convex_pd_def |
41290
e9c9577d88b5
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents:
41289
diff
changeset
|
152 |
by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj) |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
153 |
next |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
154 |
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
|
155 |
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
|
156 |
by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
157 |
qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+ |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
158 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
159 |
end |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
160 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
161 |
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
|
162 |
by (rule defl_upper_pd_def) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
163 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
164 |
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
|
165 |
by (rule defl_lower_pd_def) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
166 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
167 |
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
|
168 |
by (rule defl_convex_pd_def) |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
169 |
|
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
170 |
subsection {* Isomorphic deflations *} |
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
40774
diff
changeset
|
171 |
|
35473 | 172 |
lemma isodefl_upper: |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
173 |
"isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" |
35473 | 174 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
175 |
apply (simp add: cast_upper_defl cast_isodefl) |
35473 | 176 |
apply (simp add: emb_upper_pd_def prj_upper_pd_def) |
177 |
apply (simp add: upper_map_map) |
|
178 |
done |
|
179 |
||
180 |
lemma isodefl_lower: |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
181 |
"isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)" |
35473 | 182 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
183 |
apply (simp add: cast_lower_defl cast_isodefl) |
35473 | 184 |
apply (simp add: emb_lower_pd_def prj_lower_pd_def) |
185 |
apply (simp add: lower_map_map) |
|
186 |
done |
|
187 |
||
188 |
lemma isodefl_convex: |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
189 |
"isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)" |
35473 | 190 |
apply (rule isodeflI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
191 |
apply (simp add: cast_convex_defl cast_isodefl) |
35473 | 192 |
apply (simp add: emb_convex_pd_def prj_convex_pd_def) |
193 |
apply (simp add: convex_map_map) |
|
194 |
done |
|
195 |
||
196 |
subsection {* Domain package setup for powerdomains *} |
|
197 |
||
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
198 |
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
|
199 |
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
|
200 |
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
|
201 |
|
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
202 |
lemmas [domain_deflation] = |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset
|
203 |
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
|
204 |
|
35473 | 205 |
setup {* |
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
206 |
fold Domain_Take_Proofs.add_rec_type |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
207 |
[(@{type_name "upper_pd"}, [true]), |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
208 |
(@{type_name "lower_pd"}, [true]), |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset
|
209 |
(@{type_name "convex_pd"}, [true])] |
35473 | 210 |
*} |
211 |
||
212 |
end |