1(*  Title:      HOL/HOLCF/Algebraic.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Algebraic deflations\<close>
6
7theory Algebraic
8imports Universal Map_Functions
9begin
10
11default_sort bifinite
12
13subsection \<open>Type constructor for finite deflations\<close>
14
15typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
16by (fast intro: finite_deflation_bottom)
17
18instantiation fin_defl :: (bifinite) below
19begin
20
21definition below_fin_defl_def:
22  "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
23
24instance ..
25end
26
27instance fin_defl :: (bifinite) po
28using type_definition_fin_defl below_fin_defl_def
29by (rule typedef_po)
30
31lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
32using Rep_fin_defl by simp
33
34lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
35using finite_deflation_Rep_fin_defl
36by (rule finite_deflation_imp_deflation)
37
38interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
39by (rule finite_deflation_Rep_fin_defl)
40
41lemma fin_defl_belowI:
42  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
43unfolding below_fin_defl_def
44by (rule Rep_fin_defl.belowI)
45
46lemma fin_defl_belowD:
47  "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
48unfolding below_fin_defl_def
49by (rule Rep_fin_defl.belowD)
50
51lemma fin_defl_eqI:
52  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
53apply (rule below_antisym)
54apply (rule fin_defl_belowI, simp)
55apply (rule fin_defl_belowI, simp)
56done
57
58lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
59unfolding below_fin_defl_def .
60
61lemma Abs_fin_defl_mono:
62  "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
63    \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
64unfolding below_fin_defl_def
65by (simp add: Abs_fin_defl_inverse)
66
67lemma (in finite_deflation) compact_belowI:
68  assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
69by (rule belowI, rule assms, erule subst, rule compact)
70
71lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
72using finite_deflation_Rep_fin_defl
73by (rule finite_deflation_imp_compact)
74
75subsection \<open>Defining algebraic deflations by ideal completion\<close>
76
77typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
78by (rule below.ex_ideal)
79
80instantiation defl :: (bifinite) below
81begin
82
83definition
84  "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
85
86instance ..
87end
88
89instance defl :: (bifinite) po
90using type_definition_defl below_defl_def
91by (rule below.typedef_ideal_po)
92
93instance defl :: (bifinite) cpo
94using type_definition_defl below_defl_def
95by (rule below.typedef_ideal_cpo)
96
97definition
98  defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
99  "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
100
101lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
102proof -
103  obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
104    using compact_basis.countable ..
105  have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
106    apply (rule finite_imageI)
107    apply (rule finite_vimageI)
108    apply (rule Rep_fin_defl.finite_fixes)
109    apply (simp add: inj_on_def Rep_compact_basis_inject)
110    done
111  have range_eq: "range Rep_compact_basis = {x. compact x}"
112    using type_definition_compact_basis by (rule type_definition.Rep_range)
113  have "inj (\<lambda>d. set_encode
114    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
115    apply (rule inj_onI)
116    apply (simp only: set_encode_eq *)
117    apply (simp only: inj_image_eq_iff inj_f)
118    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
119    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
120    apply (rule Rep_fin_defl_inject [THEN iffD1])
121    apply (rule below_antisym)
122    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
123    apply (drule_tac x=z in spec, simp)
124    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
125    apply (drule_tac x=z in spec, simp)
126    done
127  thus ?thesis by - (rule exI)
128qed
129
130interpretation defl: ideal_completion below defl_principal Rep_defl
131using type_definition_defl below_defl_def
132using defl_principal_def fin_defl_countable
133by (rule below.typedef_ideal_completion)
134
135text \<open>Algebraic deflations are pointed\<close>
136
137lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
138apply (induct x rule: defl.principal_induct, simp)
139apply (rule defl.principal_mono)
140apply (simp add: below_fin_defl_def)
141apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
142done
143
144instance defl :: (bifinite) pcpo
145by intro_classes (fast intro: defl_minimal)
146
147lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
148by (rule defl_minimal [THEN bottomI, symmetric])
149
150subsection \<open>Applying algebraic deflations\<close>
151
152definition
153  cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
154where
155  "cast = defl.extension Rep_fin_defl"
156
157lemma cast_defl_principal:
158  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
159unfolding cast_def
160apply (rule defl.extension_principal)
161apply (simp only: below_fin_defl_def)
162done
163
164lemma deflation_cast: "deflation (cast\<cdot>d)"
165apply (induct d rule: defl.principal_induct)
166apply (rule adm_subst [OF _ adm_deflation], simp)
167apply (simp add: cast_defl_principal)
168apply (rule finite_deflation_imp_deflation)
169apply (rule finite_deflation_Rep_fin_defl)
170done
171
172lemma finite_deflation_cast:
173  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
174apply (drule defl.compact_imp_principal, clarify)
175apply (simp add: cast_defl_principal)
176apply (rule finite_deflation_Rep_fin_defl)
177done
178
179interpretation cast: deflation "cast\<cdot>d"
180by (rule deflation_cast)
181
182declare cast.idem [simp]
183
184lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
185apply (rule finite_deflation_imp_compact)
186apply (erule finite_deflation_cast)
187done
188
189lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
190apply (induct A rule: defl.principal_induct, simp)
191apply (induct B rule: defl.principal_induct, simp)
192apply (simp add: cast_defl_principal below_fin_defl_def)
193done
194
195lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
196apply (rule iffI)
197apply (simp only: compact_def cast_below_cast [symmetric])
198apply (erule adm_subst [OF cont_Rep_cfun2])
199apply (erule compact_cast)
200done
201
202lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
203by (simp only: cast_below_cast)
204
205lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
206by (simp add: below_antisym cast_below_imp_below)
207
208lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
209apply (subst inst_defl_pcpo)
210apply (subst cast_defl_principal)
211apply (rule Abs_fin_defl_inverse)
212apply (simp add: finite_deflation_bottom)
213done
214
215lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
216by (rule cast.below [THEN bottomI])
217
218subsection \<open>Deflation combinators\<close>
219
220definition
221  "defl_fun1 e p f =
222    defl.extension (\<lambda>a.
223      defl_principal (Abs_fin_defl
224        (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
225
226definition
227  "defl_fun2 e p f =
228    defl.extension (\<lambda>a.
229      defl.extension (\<lambda>b.
230        defl_principal (Abs_fin_defl
231          (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
232
233lemma cast_defl_fun1:
234  assumes ep: "ep_pair e p"
235  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
236  shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
237proof -
238  have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
239    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
240    apply (rule f, rule finite_deflation_Rep_fin_defl)
241    done
242  show ?thesis
243    by (induct A rule: defl.principal_induct, simp)
244       (simp only: defl_fun1_def
245                   defl.extension_principal
246                   defl.extension_mono
247                   defl.principal_mono
248                   Abs_fin_defl_mono [OF 1 1]
249                   monofun_cfun below_refl
250                   Rep_fin_defl_mono
251                   cast_defl_principal
252                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
253qed
254
255lemma cast_defl_fun2:
256  assumes ep: "ep_pair e p"
257  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
258                finite_deflation (f\<cdot>a\<cdot>b)"
259  shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
260proof -
261  have 1: "\<And>a b. finite_deflation
262      (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
263    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
264    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
265    done
266  show ?thesis
267    apply (induct A rule: defl.principal_induct, simp)
268    apply (induct B rule: defl.principal_induct, simp)
269    by (simp only: defl_fun2_def
270                   defl.extension_principal
271                   defl.extension_mono
272                   defl.principal_mono
273                   Abs_fin_defl_mono [OF 1 1]
274                   monofun_cfun below_refl
275                   Rep_fin_defl_mono
276                   cast_defl_principal
277                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
278qed
279
280end
281