1(*  Title:      HOL/HOLCF/Bifinite.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Profinite and bifinite cpos\<close>
6
7theory Bifinite
8  imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
9begin
10
11default_sort cpo
12
13subsection \<open>Chains of finite deflations\<close>
14
15locale approx_chain =
16  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
17  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
18  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
19  assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)"
20begin
21
22lemma deflation_approx: "deflation (approx i)"
23using finite_deflation_approx by (rule finite_deflation_imp_deflation)
24
25lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
26using deflation_approx by (rule deflation.idem)
27
28lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
29using deflation_approx by (rule deflation.below)
30
31lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
32apply (rule finite_deflation.finite_range)
33apply (rule finite_deflation_approx)
34done
35
36lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
37apply (rule finite_deflation.compact)
38apply (rule finite_deflation_approx)
39done
40
41lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
42by (rule admD2, simp_all)
43
44end
45
46subsection \<open>Omega-profinite and bifinite domains\<close>
47
48class bifinite = pcpo +
49  assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
50
51class profinite = cpo +
52  assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
53
54subsection \<open>Building approx chains\<close>
55
56lemma approx_chain_iso:
57  assumes a: "approx_chain a"
58  assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
59  assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"
60  shows "approx_chain (\<lambda>i. f oo a i oo g)"
61proof -
62  have 1: "f oo g = ID" by (simp add: cfun_eqI)
63  have 2: "ep_pair f g" by (simp add: ep_pair_def)
64  from 1 2 show ?thesis
65    using a unfolding approx_chain_def
66    by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
67qed
68
69lemma approx_chain_u_map:
70  assumes "approx_chain a"
71  shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))"
72  using assms unfolding approx_chain_def
73  by (simp add: lub_APP u_map_ID finite_deflation_u_map)
74
75lemma approx_chain_sfun_map:
76  assumes "approx_chain a" and "approx_chain b"
77  shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))"
78  using assms unfolding approx_chain_def
79  by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
80
81lemma approx_chain_sprod_map:
82  assumes "approx_chain a" and "approx_chain b"
83  shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))"
84  using assms unfolding approx_chain_def
85  by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
86
87lemma approx_chain_ssum_map:
88  assumes "approx_chain a" and "approx_chain b"
89  shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))"
90  using assms unfolding approx_chain_def
91  by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
92
93lemma approx_chain_cfun_map:
94  assumes "approx_chain a" and "approx_chain b"
95  shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
96  using assms unfolding approx_chain_def
97  by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
98
99lemma approx_chain_prod_map:
100  assumes "approx_chain a" and "approx_chain b"
101  shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))"
102  using assms unfolding approx_chain_def
103  by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
104
105text \<open>Approx chains for countable discrete types.\<close>
106
107definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
108  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
109
110lemma chain_discr_approx [simp]: "chain discr_approx"
111unfolding discr_approx_def
112by (rule chainI, simp add: monofun_cfun monofun_LAM)
113
114lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
115  apply (rule cfun_eqI)
116  apply (simp add: contlub_cfun_fun)
117  apply (simp add: discr_approx_def)
118  subgoal for x
119    apply (cases x)
120     apply simp
121    apply (rule lub_eqI)
122    apply (rule is_lubI)
123     apply (rule ub_rangeI, simp)
124    apply (drule ub_rangeD)
125    apply (erule rev_below_trans)
126    apply simp
127    apply (rule lessI)
128    done
129  done
130
131lemma inj_on_undiscr [simp]: "inj_on undiscr A"
132using Discr_undiscr by (rule inj_on_inverseI)
133
134lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
135proof
136  fix x :: "'a discr u"
137  show "discr_approx i\<cdot>x \<sqsubseteq> x"
138    unfolding discr_approx_def
139    by (cases x, simp, simp)
140  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
141    unfolding discr_approx_def
142    by (cases x, simp, simp)
143  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
144  proof (rule finite_subset)
145    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
146    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
147      unfolding discr_approx_def
148      by (rule subsetI, case_tac x, simp, simp split: if_split_asm)
149    show "finite ?S"
150      by (simp add: finite_vimageI)
151  qed
152qed
153
154lemma discr_approx: "approx_chain discr_approx"
155using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
156by (rule approx_chain.intro)
157
158subsection \<open>Class instance proofs\<close>
159
160instance bifinite \<subseteq> profinite
161proof
162  show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
163    using bifinite [where 'a='a]
164    by (fast intro!: approx_chain_u_map)
165qed
166
167instance u :: (profinite) bifinite
168  by standard (rule profinite)
169
170text \<open>
171  Types \<^typ>\<open>'a \<rightarrow> 'b\<close> and \<^typ>\<open>'a u \<rightarrow>! 'b\<close> are isomorphic.
172\<close>
173
174definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
175
176definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
177
178lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
179unfolding encode_cfun_def decode_cfun_def
180by (simp add: eta_cfun)
181
182lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
183unfolding encode_cfun_def decode_cfun_def
184apply (simp add: sfun_eq_iff strictify_cancel)
185apply (rule cfun_eqI, case_tac x, simp_all)
186done
187
188instance cfun :: (profinite, bifinite) bifinite
189proof
190  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
191    using profinite ..
192  obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
193    using bifinite ..
194  have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
195    using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
196  thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
197    by - (rule exI)
198qed
199
200text \<open>
201  Types \<^typ>\<open>('a * 'b) u\<close> and \<^typ>\<open>'a u \<otimes> 'b u\<close> are isomorphic.
202\<close>
203
204definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
205
206definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
207
208lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
209  unfolding encode_prod_u_def decode_prod_u_def
210  apply (cases x)
211   apply simp
212  subgoal for y by (cases y) simp
213  done
214
215lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
216  unfolding encode_prod_u_def decode_prod_u_def
217  apply (cases y)
218   apply simp
219  subgoal for a b
220    apply (cases a, simp)
221    apply (cases b, simp, simp)
222    done
223  done
224
225instance prod :: (profinite, profinite) profinite
226proof
227  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
228    using profinite ..
229  obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
230    using profinite ..
231  have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
232    using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
233  thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
234    by - (rule exI)
235qed
236
237instance prod :: (bifinite, bifinite) bifinite
238proof
239  show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
240    using bifinite [where 'a='a] and bifinite [where 'a='b]
241    by (fast intro!: approx_chain_prod_map)
242qed
243
244instance sfun :: (bifinite, bifinite) bifinite
245proof
246  show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
247    using bifinite [where 'a='a] and bifinite [where 'a='b]
248    by (fast intro!: approx_chain_sfun_map)
249qed
250
251instance sprod :: (bifinite, bifinite) bifinite
252proof
253  show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
254    using bifinite [where 'a='a] and bifinite [where 'a='b]
255    by (fast intro!: approx_chain_sprod_map)
256qed
257
258instance ssum :: (bifinite, bifinite) bifinite
259proof
260  show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
261    using bifinite [where 'a='a] and bifinite [where 'a='b]
262    by (fast intro!: approx_chain_ssum_map)
263qed
264
265lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
266by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
267
268instance unit :: bifinite
269  by standard (fast intro!: approx_chain_unit)
270
271instance discr :: (countable) profinite
272  by standard (fast intro!: discr_approx)
273
274instance lift :: (countable) bifinite
275proof
276  note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
277  obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
278    using profinite ..
279  hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
280    by (rule approx_chain_iso) simp_all
281  thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
282    by - (rule exI)
283qed
284
285end
286