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