huffman@27401
|
1 |
(* Title: HOLCF/Deflation.thy
|
huffman@27401
|
2 |
Author: Brian Huffman
|
huffman@27401
|
3 |
*)
|
huffman@27401
|
4 |
|
huffman@27401
|
5 |
header {* Continuous Deflations and Embedding-Projection Pairs *}
|
huffman@27401
|
6 |
|
huffman@27401
|
7 |
theory Deflation
|
huffman@27401
|
8 |
imports Cfun
|
huffman@27401
|
9 |
begin
|
huffman@27401
|
10 |
|
huffman@27401
|
11 |
defaultsort cpo
|
huffman@27401
|
12 |
|
huffman@27401
|
13 |
subsection {* Continuous deflations *}
|
huffman@27401
|
14 |
|
huffman@27401
|
15 |
locale deflation =
|
huffman@27401
|
16 |
fixes d :: "'a \<rightarrow> 'a"
|
huffman@27401
|
17 |
assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
|
huffman@27401
|
18 |
assumes less: "\<And>x. d\<cdot>x \<sqsubseteq> x"
|
huffman@27401
|
19 |
begin
|
huffman@27401
|
20 |
|
huffman@27401
|
21 |
lemma less_ID: "d \<sqsubseteq> ID"
|
huffman@27401
|
22 |
by (rule less_cfun_ext, simp add: less)
|
huffman@27401
|
23 |
|
huffman@27401
|
24 |
text {* The set of fixed points is the same as the range. *}
|
huffman@27401
|
25 |
|
huffman@27401
|
26 |
lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
|
huffman@27401
|
27 |
by (auto simp add: eq_sym_conv idem)
|
huffman@27401
|
28 |
|
huffman@27401
|
29 |
lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
|
huffman@27401
|
30 |
by (auto simp add: eq_sym_conv idem)
|
huffman@27401
|
31 |
|
huffman@27401
|
32 |
text {*
|
huffman@27401
|
33 |
The pointwise ordering on deflation functions coincides with
|
huffman@27401
|
34 |
the subset ordering of their sets of fixed-points.
|
huffman@27401
|
35 |
*}
|
huffman@27401
|
36 |
|
huffman@27401
|
37 |
lemma lessI:
|
huffman@27401
|
38 |
assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
|
huffman@27401
|
39 |
proof (rule less_cfun_ext)
|
huffman@27401
|
40 |
fix x
|
huffman@27401
|
41 |
from less have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
|
huffman@27401
|
42 |
also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
|
huffman@27401
|
43 |
finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
|
huffman@27401
|
44 |
qed
|
huffman@27401
|
45 |
|
huffman@27401
|
46 |
lemma lessD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
|
huffman@27401
|
47 |
proof (rule antisym_less)
|
huffman@27401
|
48 |
from less show "d\<cdot>x \<sqsubseteq> x" .
|
huffman@27401
|
49 |
next
|
huffman@27401
|
50 |
assume "f \<sqsubseteq> d"
|
huffman@27401
|
51 |
hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
|
huffman@27401
|
52 |
also assume "f\<cdot>x = x"
|
huffman@27401
|
53 |
finally show "x \<sqsubseteq> d\<cdot>x" .
|
huffman@27401
|
54 |
qed
|
huffman@27401
|
55 |
|
huffman@27401
|
56 |
end
|
huffman@27401
|
57 |
|
huffman@27401
|
58 |
lemma adm_deflation: "adm (\<lambda>d. deflation d)"
|
huffman@27401
|
59 |
by (simp add: deflation_def)
|
huffman@27401
|
60 |
|
huffman@27401
|
61 |
lemma deflation_ID: "deflation ID"
|
huffman@27401
|
62 |
by (simp add: deflation.intro)
|
huffman@27401
|
63 |
|
huffman@27401
|
64 |
lemma deflation_UU: "deflation \<bottom>"
|
huffman@27401
|
65 |
by (simp add: deflation.intro)
|
huffman@27401
|
66 |
|
huffman@27401
|
67 |
lemma deflation_less_iff:
|
huffman@27401
|
68 |
"\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
|
huffman@27401
|
69 |
apply safe
|
huffman@27401
|
70 |
apply (simp add: deflation.lessD)
|
huffman@27401
|
71 |
apply (simp add: deflation.lessI)
|
huffman@27401
|
72 |
done
|
huffman@27401
|
73 |
|
huffman@27401
|
74 |
text {*
|
huffman@27401
|
75 |
The composition of two deflations is equal to
|
huffman@27401
|
76 |
the lesser of the two (if they are comparable).
|
huffman@27401
|
77 |
*}
|
huffman@27401
|
78 |
|
huffman@27401
|
79 |
lemma deflation_less_comp1:
|
ballarin@28611
|
80 |
assumes "deflation f"
|
ballarin@28611
|
81 |
assumes "deflation g"
|
huffman@27401
|
82 |
shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
|
huffman@27401
|
83 |
proof (rule antisym_less)
|
ballarin@29237
|
84 |
interpret g: deflation g by fact
|
huffman@27401
|
85 |
from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
|
huffman@27401
|
86 |
next
|
ballarin@29237
|
87 |
interpret f: deflation f by fact
|
huffman@27401
|
88 |
assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
|
huffman@27401
|
89 |
hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
|
huffman@27401
|
90 |
also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
|
huffman@27401
|
91 |
finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
|
huffman@27401
|
92 |
qed
|
huffman@27401
|
93 |
|
huffman@27401
|
94 |
lemma deflation_less_comp2:
|
huffman@27401
|
95 |
"\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
|
huffman@27401
|
96 |
by (simp only: deflation.lessD deflation.idem)
|
huffman@27401
|
97 |
|
huffman@27401
|
98 |
|
huffman@27401
|
99 |
subsection {* Deflations with finite range *}
|
huffman@27401
|
100 |
|
huffman@27401
|
101 |
lemma finite_range_imp_finite_fixes:
|
huffman@27401
|
102 |
"finite (range f) \<Longrightarrow> finite {x. f x = x}"
|
huffman@27401
|
103 |
proof -
|
huffman@27401
|
104 |
have "{x. f x = x} \<subseteq> range f"
|
huffman@27401
|
105 |
by (clarify, erule subst, rule rangeI)
|
huffman@27401
|
106 |
moreover assume "finite (range f)"
|
huffman@27401
|
107 |
ultimately show "finite {x. f x = x}"
|
huffman@27401
|
108 |
by (rule finite_subset)
|
huffman@27401
|
109 |
qed
|
huffman@27401
|
110 |
|
huffman@27401
|
111 |
locale finite_deflation = deflation +
|
huffman@27401
|
112 |
assumes finite_fixes: "finite {x. d\<cdot>x = x}"
|
huffman@27401
|
113 |
begin
|
huffman@27401
|
114 |
|
huffman@27401
|
115 |
lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
|
huffman@27401
|
116 |
by (simp add: range_eq_fixes finite_fixes)
|
huffman@27401
|
117 |
|
huffman@27401
|
118 |
lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
|
huffman@27401
|
119 |
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
|
huffman@27401
|
120 |
|
huffman@27401
|
121 |
lemma compact: "compact (d\<cdot>x)"
|
huffman@27401
|
122 |
proof (rule compactI2)
|
huffman@27401
|
123 |
fix Y :: "nat \<Rightarrow> 'a"
|
huffman@27401
|
124 |
assume Y: "chain Y"
|
huffman@27401
|
125 |
have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
|
huffman@27401
|
126 |
proof (rule finite_range_imp_finch)
|
huffman@27401
|
127 |
show "chain (\<lambda>i. d\<cdot>(Y i))"
|
huffman@27401
|
128 |
using Y by simp
|
huffman@27401
|
129 |
have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
|
huffman@27401
|
130 |
by clarsimp
|
huffman@27401
|
131 |
thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
|
huffman@27401
|
132 |
using finite_range by (rule finite_subset)
|
huffman@27401
|
133 |
qed
|
huffman@27401
|
134 |
hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
|
huffman@27401
|
135 |
by (simp add: finite_chain_def maxinch_is_thelub Y)
|
huffman@27401
|
136 |
then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
|
huffman@27401
|
137 |
|
huffman@27401
|
138 |
assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
|
huffman@27401
|
139 |
hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
|
huffman@27401
|
140 |
by (rule monofun_cfun_arg)
|
huffman@27401
|
141 |
hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
|
huffman@27401
|
142 |
by (simp add: contlub_cfun_arg Y idem)
|
huffman@27401
|
143 |
hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
|
huffman@27401
|
144 |
using j by simp
|
huffman@27401
|
145 |
hence "d\<cdot>x \<sqsubseteq> Y j"
|
huffman@27401
|
146 |
using less by (rule trans_less)
|
huffman@27401
|
147 |
thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
|
huffman@27401
|
148 |
qed
|
huffman@27401
|
149 |
|
huffman@27401
|
150 |
end
|
huffman@27401
|
151 |
|
huffman@27401
|
152 |
|
huffman@27401
|
153 |
subsection {* Continuous embedding-projection pairs *}
|
huffman@27401
|
154 |
|
huffman@27401
|
155 |
locale ep_pair =
|
huffman@27401
|
156 |
fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
|
huffman@27401
|
157 |
assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
|
huffman@27401
|
158 |
and e_p_less: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
|
huffman@27401
|
159 |
begin
|
huffman@27401
|
160 |
|
huffman@27401
|
161 |
lemma e_less_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
|
huffman@27401
|
162 |
proof
|
huffman@27401
|
163 |
assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
|
huffman@27401
|
164 |
hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
|
huffman@27401
|
165 |
thus "x \<sqsubseteq> y" by simp
|
huffman@27401
|
166 |
next
|
huffman@27401
|
167 |
assume "x \<sqsubseteq> y"
|
huffman@27401
|
168 |
thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
|
huffman@27401
|
169 |
qed
|
huffman@27401
|
170 |
|
huffman@27401
|
171 |
lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
|
huffman@27401
|
172 |
unfolding po_eq_conv e_less_iff ..
|
huffman@27401
|
173 |
|
huffman@27401
|
174 |
lemma p_eq_iff:
|
huffman@27401
|
175 |
"\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
|
huffman@27401
|
176 |
by (safe, erule subst, erule subst, simp)
|
huffman@27401
|
177 |
|
huffman@27401
|
178 |
lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
|
huffman@27401
|
179 |
by (auto, rule exI, erule sym)
|
huffman@27401
|
180 |
|
huffman@27401
|
181 |
lemma e_less_iff_less_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
|
huffman@27401
|
182 |
proof
|
huffman@27401
|
183 |
assume "e\<cdot>x \<sqsubseteq> y"
|
huffman@27401
|
184 |
then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
|
huffman@27401
|
185 |
then show "x \<sqsubseteq> p\<cdot>y" by simp
|
huffman@27401
|
186 |
next
|
huffman@27401
|
187 |
assume "x \<sqsubseteq> p\<cdot>y"
|
huffman@27401
|
188 |
then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
|
huffman@27401
|
189 |
then show "e\<cdot>x \<sqsubseteq> y" using e_p_less by (rule trans_less)
|
huffman@27401
|
190 |
qed
|
huffman@27401
|
191 |
|
huffman@27401
|
192 |
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
|
huffman@27401
|
193 |
proof -
|
huffman@27401
|
194 |
assume "compact (e\<cdot>x)"
|
huffman@27401
|
195 |
hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
|
huffman@27401
|
196 |
hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
|
huffman@27401
|
197 |
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
|
huffman@27401
|
198 |
thus "compact x" by (rule compactI)
|
huffman@27401
|
199 |
qed
|
huffman@27401
|
200 |
|
huffman@27401
|
201 |
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
|
huffman@27401
|
202 |
proof -
|
huffman@27401
|
203 |
assume "compact x"
|
huffman@27401
|
204 |
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
|
huffman@27401
|
205 |
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
|
huffman@27401
|
206 |
hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_less_iff_less_p)
|
huffman@27401
|
207 |
thus "compact (e\<cdot>x)" by (rule compactI)
|
huffman@27401
|
208 |
qed
|
huffman@27401
|
209 |
|
huffman@27401
|
210 |
lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
|
huffman@27401
|
211 |
by (rule iffI [OF compact_e_rev compact_e])
|
huffman@27401
|
212 |
|
huffman@27401
|
213 |
text {* Deflations from ep-pairs *}
|
huffman@27401
|
214 |
|
huffman@27401
|
215 |
lemma deflation_e_p: "deflation (e oo p)"
|
huffman@27401
|
216 |
by (simp add: deflation.intro e_p_less)
|
huffman@27401
|
217 |
|
huffman@27401
|
218 |
lemma deflation_e_d_p:
|
ballarin@28611
|
219 |
assumes "deflation d"
|
huffman@27401
|
220 |
shows "deflation (e oo d oo p)"
|
huffman@27401
|
221 |
proof
|
ballarin@29237
|
222 |
interpret deflation d by fact
|
huffman@27401
|
223 |
fix x :: 'b
|
huffman@27401
|
224 |
show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
|
huffman@27401
|
225 |
by (simp add: idem)
|
huffman@27401
|
226 |
show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
|
huffman@27401
|
227 |
by (simp add: e_less_iff_less_p less)
|
huffman@27401
|
228 |
qed
|
huffman@27401
|
229 |
|
huffman@27401
|
230 |
lemma finite_deflation_e_d_p:
|
ballarin@28611
|
231 |
assumes "finite_deflation d"
|
huffman@27401
|
232 |
shows "finite_deflation (e oo d oo p)"
|
huffman@27401
|
233 |
proof
|
ballarin@29237
|
234 |
interpret finite_deflation d by fact
|
huffman@27401
|
235 |
fix x :: 'b
|
huffman@27401
|
236 |
show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
|
huffman@27401
|
237 |
by (simp add: idem)
|
huffman@27401
|
238 |
show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
|
huffman@27401
|
239 |
by (simp add: e_less_iff_less_p less)
|
huffman@27401
|
240 |
have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
|
huffman@27401
|
241 |
by (simp add: finite_image)
|
huffman@27401
|
242 |
hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
|
huffman@27401
|
243 |
by (simp add: image_image)
|
huffman@27401
|
244 |
thus "finite {x. (e oo d oo p)\<cdot>x = x}"
|
huffman@27401
|
245 |
by (rule finite_range_imp_finite_fixes)
|
huffman@27401
|
246 |
qed
|
huffman@27401
|
247 |
|
huffman@27401
|
248 |
lemma deflation_p_d_e:
|
ballarin@28611
|
249 |
assumes "deflation d"
|
huffman@27401
|
250 |
assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
|
huffman@27401
|
251 |
shows "deflation (p oo d oo e)"
|
ballarin@28611
|
252 |
proof -
|
ballarin@29237
|
253 |
interpret d: deflation d by fact
|
huffman@28613
|
254 |
{
|
huffman@28613
|
255 |
fix x
|
huffman@28613
|
256 |
have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
|
huffman@28613
|
257 |
by (rule d.less)
|
huffman@28613
|
258 |
hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
|
huffman@28613
|
259 |
by (rule monofun_cfun_arg)
|
huffman@28613
|
260 |
hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
|
huffman@28613
|
261 |
by simp
|
huffman@28613
|
262 |
}
|
huffman@28613
|
263 |
note p_d_e_less = this
|
ballarin@28611
|
264 |
show ?thesis
|
huffman@28613
|
265 |
proof
|
huffman@28613
|
266 |
fix x
|
huffman@28613
|
267 |
show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
|
huffman@28613
|
268 |
by (rule p_d_e_less)
|
huffman@28613
|
269 |
next
|
huffman@28613
|
270 |
fix x
|
huffman@28613
|
271 |
show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
|
huffman@28613
|
272 |
proof (rule antisym_less)
|
huffman@28613
|
273 |
show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
|
huffman@28613
|
274 |
by (rule p_d_e_less)
|
huffman@28613
|
275 |
have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
|
huffman@28613
|
276 |
by (intro monofun_cfun_arg d)
|
huffman@28613
|
277 |
hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
|
huffman@28613
|
278 |
by (simp only: d.idem)
|
huffman@28613
|
279 |
thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
|
huffman@28613
|
280 |
by simp
|
huffman@28613
|
281 |
qed
|
huffman@28613
|
282 |
qed
|
ballarin@28611
|
283 |
qed
|
huffman@27401
|
284 |
|
huffman@27401
|
285 |
lemma finite_deflation_p_d_e:
|
ballarin@28611
|
286 |
assumes "finite_deflation d"
|
huffman@27401
|
287 |
assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
|
huffman@27401
|
288 |
shows "finite_deflation (p oo d oo e)"
|
ballarin@28611
|
289 |
proof -
|
ballarin@29237
|
290 |
interpret d: finite_deflation d by fact
|
ballarin@28611
|
291 |
show ?thesis
|
huffman@28613
|
292 |
proof (intro_locales)
|
huffman@28613
|
293 |
have "deflation d" ..
|
huffman@28613
|
294 |
thus "deflation (p oo d oo e)"
|
huffman@28613
|
295 |
using d by (rule deflation_p_d_e)
|
huffman@28613
|
296 |
next
|
huffman@28613
|
297 |
show "finite_deflation_axioms (p oo d oo e)"
|
huffman@28613
|
298 |
proof
|
huffman@28613
|
299 |
have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
|
huffman@28613
|
300 |
by (rule d.finite_image)
|
huffman@28613
|
301 |
hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
|
huffman@28613
|
302 |
by (rule finite_imageI)
|
huffman@28613
|
303 |
hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
|
huffman@28613
|
304 |
by (simp add: image_image)
|
huffman@28613
|
305 |
thus "finite {x. (p oo d oo e)\<cdot>x = x}"
|
huffman@28613
|
306 |
by (rule finite_range_imp_finite_fixes)
|
huffman@28613
|
307 |
qed
|
huffman@28613
|
308 |
qed
|
ballarin@28611
|
309 |
qed
|
huffman@27401
|
310 |
|
huffman@27401
|
311 |
end
|
huffman@27401
|
312 |
|
huffman@27401
|
313 |
subsection {* Uniqueness of ep-pairs *}
|
huffman@27401
|
314 |
|
huffman@28613
|
315 |
lemma ep_pair_unique_e_lemma:
|
huffman@28613
|
316 |
assumes "ep_pair e1 p" and "ep_pair e2 p"
|
huffman@28613
|
317 |
shows "e1 \<sqsubseteq> e2"
|
huffman@28613
|
318 |
proof (rule less_cfun_ext)
|
ballarin@29237
|
319 |
interpret e1: ep_pair e1 p by fact
|
ballarin@29237
|
320 |
interpret e2: ep_pair e2 p by fact
|
huffman@28613
|
321 |
fix x
|
huffman@28613
|
322 |
have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
|
huffman@28613
|
323 |
by (rule e1.e_p_less)
|
huffman@28613
|
324 |
thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
|
huffman@28613
|
325 |
by (simp only: e2.e_inverse)
|
huffman@28613
|
326 |
qed
|
huffman@28613
|
327 |
|
huffman@27401
|
328 |
lemma ep_pair_unique_e:
|
huffman@27401
|
329 |
"\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
|
huffman@28613
|
330 |
by (fast intro: antisym_less elim: ep_pair_unique_e_lemma)
|
huffman@28613
|
331 |
|
huffman@28613
|
332 |
lemma ep_pair_unique_p_lemma:
|
huffman@28613
|
333 |
assumes "ep_pair e p1" and "ep_pair e p2"
|
huffman@28613
|
334 |
shows "p1 \<sqsubseteq> p2"
|
huffman@28613
|
335 |
proof (rule less_cfun_ext)
|
ballarin@29237
|
336 |
interpret p1: ep_pair e p1 by fact
|
ballarin@29237
|
337 |
interpret p2: ep_pair e p2 by fact
|
huffman@28613
|
338 |
fix x
|
huffman@28613
|
339 |
have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
|
huffman@28613
|
340 |
by (rule p1.e_p_less)
|
huffman@28613
|
341 |
hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
|
huffman@28613
|
342 |
by (rule monofun_cfun_arg)
|
huffman@28613
|
343 |
thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
|
huffman@28613
|
344 |
by (simp only: p2.e_inverse)
|
huffman@28613
|
345 |
qed
|
huffman@27401
|
346 |
|
huffman@27401
|
347 |
lemma ep_pair_unique_p:
|
huffman@27401
|
348 |
"\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
|
huffman@28613
|
349 |
by (fast intro: antisym_less elim: ep_pair_unique_p_lemma)
|
huffman@27401
|
350 |
|
huffman@27401
|
351 |
subsection {* Composing ep-pairs *}
|
huffman@27401
|
352 |
|
huffman@27401
|
353 |
lemma ep_pair_ID_ID: "ep_pair ID ID"
|
huffman@27401
|
354 |
by default simp_all
|
huffman@27401
|
355 |
|
huffman@27401
|
356 |
lemma ep_pair_comp:
|
huffman@28613
|
357 |
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
|
huffman@28613
|
358 |
shows "ep_pair (e2 oo e1) (p1 oo p2)"
|
huffman@28613
|
359 |
proof
|
ballarin@29237
|
360 |
interpret ep1: ep_pair e1 p1 by fact
|
ballarin@29237
|
361 |
interpret ep2: ep_pair e2 p2 by fact
|
huffman@28613
|
362 |
fix x y
|
huffman@28613
|
363 |
show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
|
huffman@28613
|
364 |
by simp
|
huffman@28613
|
365 |
have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
|
huffman@28613
|
366 |
by (rule ep1.e_p_less)
|
huffman@28613
|
367 |
hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
|
huffman@28613
|
368 |
by (rule monofun_cfun_arg)
|
huffman@28613
|
369 |
also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
|
huffman@28613
|
370 |
by (rule ep2.e_p_less)
|
huffman@28613
|
371 |
finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
|
huffman@28613
|
372 |
by simp
|
huffman@28613
|
373 |
qed
|
huffman@27401
|
374 |
|
haftmann@27681
|
375 |
locale pcpo_ep_pair = ep_pair +
|
huffman@27401
|
376 |
constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
|
huffman@27401
|
377 |
constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
|
huffman@27401
|
378 |
begin
|
huffman@27401
|
379 |
|
huffman@27401
|
380 |
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
|
huffman@27401
|
381 |
proof -
|
huffman@27401
|
382 |
have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
|
huffman@27401
|
383 |
hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
|
huffman@27401
|
384 |
also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_less)
|
huffman@27401
|
385 |
finally show "e\<cdot>\<bottom> = \<bottom>" by simp
|
huffman@27401
|
386 |
qed
|
huffman@27401
|
387 |
|
huffman@27401
|
388 |
lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
|
huffman@27401
|
389 |
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
|
huffman@27401
|
390 |
|
huffman@27401
|
391 |
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
|
huffman@27401
|
392 |
by simp
|
huffman@27401
|
393 |
|
huffman@27401
|
394 |
lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
|
huffman@27401
|
395 |
by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
|
huffman@27401
|
396 |
|
huffman@27401
|
397 |
lemmas stricts = e_strict p_strict
|
huffman@27401
|
398 |
|
huffman@27401
|
399 |
end
|
huffman@27401
|
400 |
|
huffman@27401
|
401 |
end
|