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