changeset 39989 | ad60d7311f43 |
parent 39987 | 8c2f449af35a |
child 40002 | c5b5f7a3a3b1 |
39988:a4b2971952f4 | 39989:ad60d7311f43 |
---|---|
16 *} |
16 *} |
17 |
17 |
18 class bifinite = pcpo + |
18 class bifinite = pcpo + |
19 fixes emb :: "'a::pcpo \<rightarrow> udom" |
19 fixes emb :: "'a::pcpo \<rightarrow> udom" |
20 fixes prj :: "udom \<rightarrow> 'a::pcpo" |
20 fixes prj :: "udom \<rightarrow> 'a::pcpo" |
21 fixes sfp :: "'a itself \<Rightarrow> sfp" |
21 fixes defl :: "'a itself \<Rightarrow> defl" |
22 assumes ep_pair_emb_prj: "ep_pair emb prj" |
22 assumes ep_pair_emb_prj: "ep_pair emb prj" |
23 assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj" |
23 assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj" |
24 |
24 |
25 syntax "_SFP" :: "type \<Rightarrow> sfp" ("(1SFP/(1'(_')))") |
25 syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))") |
26 translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)" |
26 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)" |
27 |
27 |
28 interpretation bifinite: |
28 interpretation bifinite: |
29 pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite" |
29 pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite" |
30 unfolding pcpo_ep_pair_def |
30 unfolding pcpo_ep_pair_def |
31 by (rule ep_pair_emb_prj) |
31 by (rule ep_pair_emb_prj) |
45 |
45 |
46 interpretation compact_basis: |
46 interpretation compact_basis: |
47 ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _" |
47 ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _" |
48 proof - |
48 proof - |
49 obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" |
49 obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" |
50 and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))" |
50 and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))" |
51 by (rule sfp.obtain_principal_chain) |
51 by (rule defl.obtain_principal_chain) |
52 def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a" |
52 def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a" |
53 interpret sfp_approx: approx_chain approx |
53 interpret defl_approx: approx_chain approx |
54 proof (rule approx_chain.intro) |
54 proof (rule approx_chain.intro) |
55 show "chain (\<lambda>i. approx i)" |
55 show "chain (\<lambda>i. approx i)" |
56 unfolding approx_def by (simp add: Y) |
56 unfolding approx_def by (simp add: Y) |
57 show "(\<Squnion>i. approx i) = ID" |
57 show "(\<Squnion>i. approx i) = ID" |
58 unfolding approx_def |
58 unfolding approx_def |
59 by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq) |
59 by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq) |
60 show "\<And>i. finite_deflation (approx i)" |
60 show "\<And>i. finite_deflation (approx i)" |
61 unfolding approx_def |
61 unfolding approx_def |
62 apply (rule bifinite.finite_deflation_p_d_e) |
62 apply (rule bifinite.finite_deflation_p_d_e) |
63 apply (rule finite_deflation_cast) |
63 apply (rule finite_deflation_cast) |
64 apply (rule sfp.compact_principal) |
64 apply (rule defl.compact_principal) |
65 apply (rule below_trans [OF monofun_cfun_fun]) |
65 apply (rule below_trans [OF monofun_cfun_fun]) |
66 apply (rule is_ub_thelub, simp add: Y) |
66 apply (rule is_ub_thelub, simp add: Y) |
67 apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP) |
67 apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL) |
68 done |
68 done |
69 qed |
69 qed |
70 (* FIXME: why does show ?thesis fail here? *) |
70 (* FIXME: why does show ?thesis fail here? *) |
71 show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" .. |
71 show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" .. |
72 qed |
72 qed |
73 |
73 |
74 subsection {* Type combinators *} |
74 subsection {* Type combinators *} |
75 |
75 |
76 definition |
76 definition |
77 sfp_fun1 :: |
77 defl_fun1 :: |
78 "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)" |
78 "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)" |
79 where |
79 where |
80 "sfp_fun1 approx f = |
80 "defl_fun1 approx f = |
81 sfp.basis_fun (\<lambda>a. |
81 defl.basis_fun (\<lambda>a. |
82 sfp_principal (Abs_fin_defl |
82 defl_principal (Abs_fin_defl |
83 (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))" |
83 (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))" |
84 |
84 |
85 definition |
85 definition |
86 sfp_fun2 :: |
86 defl_fun2 :: |
87 "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) |
87 "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) |
88 \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)" |
88 \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)" |
89 where |
89 where |
90 "sfp_fun2 approx f = |
90 "defl_fun2 approx f = |
91 sfp.basis_fun (\<lambda>a. |
91 defl.basis_fun (\<lambda>a. |
92 sfp.basis_fun (\<lambda>b. |
92 defl.basis_fun (\<lambda>b. |
93 sfp_principal (Abs_fin_defl |
93 defl_principal (Abs_fin_defl |
94 (udom_emb approx oo |
94 (udom_emb approx oo |
95 f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))" |
95 f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))" |
96 |
96 |
97 lemma cast_sfp_fun1: |
97 lemma cast_defl_fun1: |
98 assumes approx: "approx_chain approx" |
98 assumes approx: "approx_chain approx" |
99 assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)" |
99 assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)" |
100 shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx" |
100 shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx" |
101 proof - |
101 proof - |
102 have 1: "\<And>a. finite_deflation |
102 have 1: "\<And>a. finite_deflation |
103 (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)" |
103 (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)" |
104 apply (rule ep_pair.finite_deflation_e_d_p) |
104 apply (rule ep_pair.finite_deflation_e_d_p) |
105 apply (rule approx_chain.ep_pair_udom [OF approx]) |
105 apply (rule approx_chain.ep_pair_udom [OF approx]) |
106 apply (rule f, rule finite_deflation_Rep_fin_defl) |
106 apply (rule f, rule finite_deflation_Rep_fin_defl) |
107 done |
107 done |
108 show ?thesis |
108 show ?thesis |
109 by (induct A rule: sfp.principal_induct, simp) |
109 by (induct A rule: defl.principal_induct, simp) |
110 (simp only: sfp_fun1_def |
110 (simp only: defl_fun1_def |
111 sfp.basis_fun_principal |
111 defl.basis_fun_principal |
112 sfp.basis_fun_mono |
112 defl.basis_fun_mono |
113 sfp.principal_mono |
113 defl.principal_mono |
114 Abs_fin_defl_mono [OF 1 1] |
114 Abs_fin_defl_mono [OF 1 1] |
115 monofun_cfun below_refl |
115 monofun_cfun below_refl |
116 Rep_fin_defl_mono |
116 Rep_fin_defl_mono |
117 cast_sfp_principal |
117 cast_defl_principal |
118 Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
118 Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
119 qed |
119 qed |
120 |
120 |
121 lemma cast_sfp_fun2: |
121 lemma cast_defl_fun2: |
122 assumes approx: "approx_chain approx" |
122 assumes approx: "approx_chain approx" |
123 assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow> |
123 assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow> |
124 finite_deflation (f\<cdot>a\<cdot>b)" |
124 finite_deflation (f\<cdot>a\<cdot>b)" |
125 shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) = |
125 shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) = |
126 udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx" |
126 udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx" |
127 proof - |
127 proof - |
128 have 1: "\<And>a b. finite_deflation (udom_emb approx oo |
128 have 1: "\<And>a b. finite_deflation (udom_emb approx oo |
129 f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)" |
129 f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)" |
130 apply (rule ep_pair.finite_deflation_e_d_p) |
130 apply (rule ep_pair.finite_deflation_e_d_p) |
131 apply (rule ep_pair_udom [OF approx]) |
131 apply (rule ep_pair_udom [OF approx]) |
132 apply (rule f, (rule finite_deflation_Rep_fin_defl)+) |
132 apply (rule f, (rule finite_deflation_Rep_fin_defl)+) |
133 done |
133 done |
134 show ?thesis |
134 show ?thesis |
135 by (induct A B rule: sfp.principal_induct2, simp, simp) |
135 by (induct A B rule: defl.principal_induct2, simp, simp) |
136 (simp only: sfp_fun2_def |
136 (simp only: defl_fun2_def |
137 sfp.basis_fun_principal |
137 defl.basis_fun_principal |
138 sfp.basis_fun_mono |
138 defl.basis_fun_mono |
139 sfp.principal_mono |
139 defl.principal_mono |
140 Abs_fin_defl_mono [OF 1 1] |
140 Abs_fin_defl_mono [OF 1 1] |
141 monofun_cfun below_refl |
141 monofun_cfun below_refl |
142 Rep_fin_defl_mono |
142 Rep_fin_defl_mono |
143 cast_sfp_principal |
143 cast_defl_principal |
144 Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
144 Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
145 qed |
145 qed |
146 |
146 |
147 subsection {* The universal domain is bifinite *} |
147 subsection {* The universal domain is bifinite *} |
148 |
148 |
154 |
154 |
155 definition [simp]: |
155 definition [simp]: |
156 "prj = (ID :: udom \<rightarrow> udom)" |
156 "prj = (ID :: udom \<rightarrow> udom)" |
157 |
157 |
158 definition |
158 definition |
159 "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))" |
159 "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))" |
160 |
160 |
161 instance proof |
161 instance proof |
162 show "ep_pair emb (prj :: udom \<rightarrow> udom)" |
162 show "ep_pair emb (prj :: udom \<rightarrow> udom)" |
163 by (simp add: ep_pair.intro) |
163 by (simp add: ep_pair.intro) |
164 next |
164 next |
165 show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)" |
165 show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)" |
166 unfolding sfp_udom_def |
166 unfolding defl_udom_def |
167 apply (subst contlub_cfun_arg) |
167 apply (subst contlub_cfun_arg) |
168 apply (rule chainI) |
168 apply (rule chainI) |
169 apply (rule sfp.principal_mono) |
169 apply (rule defl.principal_mono) |
170 apply (simp add: below_fin_defl_def) |
170 apply (simp add: below_fin_defl_def) |
171 apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
171 apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
172 apply (rule chainE) |
172 apply (rule chainE) |
173 apply (rule chain_udom_approx) |
173 apply (rule chain_udom_approx) |
174 apply (subst cast_sfp_principal) |
174 apply (subst cast_defl_principal) |
175 apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
175 apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
176 done |
176 done |
177 qed |
177 qed |
178 |
178 |
179 end |
179 end |
195 show "\<And>i. finite_deflation (cfun_approx i)" |
195 show "\<And>i. finite_deflation (cfun_approx i)" |
196 unfolding cfun_approx_def |
196 unfolding cfun_approx_def |
197 by (intro finite_deflation_cfun_map finite_deflation_udom_approx) |
197 by (intro finite_deflation_cfun_map finite_deflation_udom_approx) |
198 qed |
198 qed |
199 |
199 |
200 definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp" |
200 definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
201 where "cfun_sfp = sfp_fun2 cfun_approx cfun_map" |
201 where "cfun_defl = defl_fun2 cfun_approx cfun_map" |
202 |
202 |
203 lemma cast_cfun_sfp: |
203 lemma cast_cfun_defl: |
204 "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) = |
204 "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = |
205 udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx" |
205 udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx" |
206 unfolding cfun_sfp_def |
206 unfolding cfun_defl_def |
207 apply (rule cast_sfp_fun2 [OF cfun_approx]) |
207 apply (rule cast_defl_fun2 [OF cfun_approx]) |
208 apply (erule (1) finite_deflation_cfun_map) |
208 apply (erule (1) finite_deflation_cfun_map) |
209 done |
209 done |
210 |
210 |
211 instantiation cfun :: (bifinite, bifinite) bifinite |
211 instantiation cfun :: (bifinite, bifinite) bifinite |
212 begin |
212 begin |
216 |
216 |
217 definition |
217 definition |
218 "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx" |
218 "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx" |
219 |
219 |
220 definition |
220 definition |
221 "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
221 "defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
222 |
222 |
223 instance proof |
223 instance proof |
224 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
224 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
225 unfolding emb_cfun_def prj_cfun_def |
225 unfolding emb_cfun_def prj_cfun_def |
226 using ep_pair_udom [OF cfun_approx] |
226 using ep_pair_udom [OF cfun_approx] |
227 by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj) |
227 by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj) |
228 next |
228 next |
229 show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
229 show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
230 unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp |
230 unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl |
231 by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map) |
231 by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map) |
232 qed |
232 qed |
233 |
233 |
234 end |
234 end |
235 |
235 |
236 lemma SFP_cfun: |
236 lemma DEFL_cfun: |
237 "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
237 "DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
238 by (rule sfp_cfun_def) |
238 by (rule defl_cfun_def) |
239 |
239 |
240 subsection {* Cartesian product is a bifinite domain *} |
240 subsection {* Cartesian product is a bifinite domain *} |
241 |
241 |
242 definition |
242 definition |
243 prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom" |
243 prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom" |
254 show "\<And>i. finite_deflation (prod_approx i)" |
254 show "\<And>i. finite_deflation (prod_approx i)" |
255 unfolding prod_approx_def |
255 unfolding prod_approx_def |
256 by (intro finite_deflation_cprod_map finite_deflation_udom_approx) |
256 by (intro finite_deflation_cprod_map finite_deflation_udom_approx) |
257 qed |
257 qed |
258 |
258 |
259 definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp" |
259 definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
260 where "prod_sfp = sfp_fun2 prod_approx cprod_map" |
260 where "prod_defl = defl_fun2 prod_approx cprod_map" |
261 |
261 |
262 lemma cast_prod_sfp: |
262 lemma cast_prod_defl: |
263 "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo |
263 "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo |
264 cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx" |
264 cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx" |
265 unfolding prod_sfp_def |
265 unfolding prod_defl_def |
266 apply (rule cast_sfp_fun2 [OF prod_approx]) |
266 apply (rule cast_defl_fun2 [OF prod_approx]) |
267 apply (erule (1) finite_deflation_cprod_map) |
267 apply (erule (1) finite_deflation_cprod_map) |
268 done |
268 done |
269 |
269 |
270 instantiation prod :: (bifinite, bifinite) bifinite |
270 instantiation prod :: (bifinite, bifinite) bifinite |
271 begin |
271 begin |
275 |
275 |
276 definition |
276 definition |
277 "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx" |
277 "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx" |
278 |
278 |
279 definition |
279 definition |
280 "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
280 "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
281 |
281 |
282 instance proof |
282 instance proof |
283 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)" |
283 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)" |
284 unfolding emb_prod_def prj_prod_def |
284 unfolding emb_prod_def prj_prod_def |
285 using ep_pair_udom [OF prod_approx] |
285 using ep_pair_udom [OF prod_approx] |
286 by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj) |
286 by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj) |
287 next |
287 next |
288 show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)" |
288 show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)" |
289 unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp |
289 unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl |
290 by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map) |
290 by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map) |
291 qed |
291 qed |
292 |
292 |
293 end |
293 end |
294 |
294 |
295 lemma SFP_prod: |
295 lemma DEFL_prod: |
296 "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
296 "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
297 by (rule sfp_prod_def) |
297 by (rule defl_prod_def) |
298 |
298 |
299 subsection {* Strict product is a bifinite domain *} |
299 subsection {* Strict product is a bifinite domain *} |
300 |
300 |
301 definition |
301 definition |
302 sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom" |
302 sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom" |
313 show "\<And>i. finite_deflation (sprod_approx i)" |
313 show "\<And>i. finite_deflation (sprod_approx i)" |
314 unfolding sprod_approx_def |
314 unfolding sprod_approx_def |
315 by (intro finite_deflation_sprod_map finite_deflation_udom_approx) |
315 by (intro finite_deflation_sprod_map finite_deflation_udom_approx) |
316 qed |
316 qed |
317 |
317 |
318 definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp" |
318 definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
319 where "sprod_sfp = sfp_fun2 sprod_approx sprod_map" |
319 where "sprod_defl = defl_fun2 sprod_approx sprod_map" |
320 |
320 |
321 lemma cast_sprod_sfp: |
321 lemma cast_sprod_defl: |
322 "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) = |
322 "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = |
323 udom_emb sprod_approx oo |
323 udom_emb sprod_approx oo |
324 sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo |
324 sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo |
325 udom_prj sprod_approx" |
325 udom_prj sprod_approx" |
326 unfolding sprod_sfp_def |
326 unfolding sprod_defl_def |
327 apply (rule cast_sfp_fun2 [OF sprod_approx]) |
327 apply (rule cast_defl_fun2 [OF sprod_approx]) |
328 apply (erule (1) finite_deflation_sprod_map) |
328 apply (erule (1) finite_deflation_sprod_map) |
329 done |
329 done |
330 |
330 |
331 instantiation sprod :: (bifinite, bifinite) bifinite |
331 instantiation sprod :: (bifinite, bifinite) bifinite |
332 begin |
332 begin |
336 |
336 |
337 definition |
337 definition |
338 "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx" |
338 "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx" |
339 |
339 |
340 definition |
340 definition |
341 "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
341 "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
342 |
342 |
343 instance proof |
343 instance proof |
344 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
344 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
345 unfolding emb_sprod_def prj_sprod_def |
345 unfolding emb_sprod_def prj_sprod_def |
346 using ep_pair_udom [OF sprod_approx] |
346 using ep_pair_udom [OF sprod_approx] |
347 by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj) |
347 by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj) |
348 next |
348 next |
349 show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
349 show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
350 unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp |
350 unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl |
351 by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map) |
351 by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map) |
352 qed |
352 qed |
353 |
353 |
354 end |
354 end |
355 |
355 |
356 lemma SFP_sprod: |
356 lemma DEFL_sprod: |
357 "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
357 "DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
358 by (rule sfp_sprod_def) |
358 by (rule defl_sprod_def) |
359 |
359 |
360 subsection {* Lifted cpo is a bifinite domain *} |
360 subsection {* Lifted cpo is a bifinite domain *} |
361 |
361 |
362 definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>" |
362 definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>" |
363 where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))" |
363 where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))" |
372 show "\<And>i. finite_deflation (u_approx i)" |
372 show "\<And>i. finite_deflation (u_approx i)" |
373 unfolding u_approx_def |
373 unfolding u_approx_def |
374 by (intro finite_deflation_u_map finite_deflation_udom_approx) |
374 by (intro finite_deflation_u_map finite_deflation_udom_approx) |
375 qed |
375 qed |
376 |
376 |
377 definition u_sfp :: "sfp \<rightarrow> sfp" |
377 definition u_defl :: "defl \<rightarrow> defl" |
378 where "u_sfp = sfp_fun1 u_approx u_map" |
378 where "u_defl = defl_fun1 u_approx u_map" |
379 |
379 |
380 lemma cast_u_sfp: |
380 lemma cast_u_defl: |
381 "cast\<cdot>(u_sfp\<cdot>A) = |
381 "cast\<cdot>(u_defl\<cdot>A) = |
382 udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx" |
382 udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx" |
383 unfolding u_sfp_def |
383 unfolding u_defl_def |
384 apply (rule cast_sfp_fun1 [OF u_approx]) |
384 apply (rule cast_defl_fun1 [OF u_approx]) |
385 apply (erule finite_deflation_u_map) |
385 apply (erule finite_deflation_u_map) |
386 done |
386 done |
387 |
387 |
388 instantiation u :: (bifinite) bifinite |
388 instantiation u :: (bifinite) bifinite |
389 begin |
389 begin |
393 |
393 |
394 definition |
394 definition |
395 "prj = u_map\<cdot>prj oo udom_prj u_approx" |
395 "prj = u_map\<cdot>prj oo udom_prj u_approx" |
396 |
396 |
397 definition |
397 definition |
398 "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)" |
398 "defl (t::'a u itself) = u_defl\<cdot>DEFL('a)" |
399 |
399 |
400 instance proof |
400 instance proof |
401 show "ep_pair emb (prj :: udom \<rightarrow> 'a u)" |
401 show "ep_pair emb (prj :: udom \<rightarrow> 'a u)" |
402 unfolding emb_u_def prj_u_def |
402 unfolding emb_u_def prj_u_def |
403 using ep_pair_udom [OF u_approx] |
403 using ep_pair_udom [OF u_approx] |
404 by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj) |
404 by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj) |
405 next |
405 next |
406 show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)" |
406 show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)" |
407 unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp |
407 unfolding emb_u_def prj_u_def defl_u_def cast_u_defl |
408 by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map) |
408 by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map) |
409 qed |
409 qed |
410 |
410 |
411 end |
411 end |
412 |
412 |
413 lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)" |
413 lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>DEFL('a)" |
414 by (rule sfp_u_def) |
414 by (rule defl_u_def) |
415 |
415 |
416 subsection {* Lifted countable types are bifinite domains *} |
416 subsection {* Lifted countable types are bifinite domains *} |
417 |
417 |
418 definition |
418 definition |
419 lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift" |
419 lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift" |
470 |
470 |
471 definition |
471 definition |
472 "prj = udom_prj lift_approx" |
472 "prj = udom_prj lift_approx" |
473 |
473 |
474 definition |
474 definition |
475 "sfp (t::'a lift itself) = |
475 "defl (t::'a lift itself) = |
476 (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))" |
476 (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))" |
477 |
477 |
478 instance proof |
478 instance proof |
479 show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)" |
479 show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)" |
480 unfolding emb_lift_def prj_lift_def |
480 unfolding emb_lift_def prj_lift_def |
481 by (rule ep_pair_udom [OF lift_approx]) |
481 by (rule ep_pair_udom [OF lift_approx]) |
482 show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)" |
482 show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)" |
483 unfolding sfp_lift_def |
483 unfolding defl_lift_def |
484 apply (subst contlub_cfun_arg) |
484 apply (subst contlub_cfun_arg) |
485 apply (rule chainI) |
485 apply (rule chainI) |
486 apply (rule sfp.principal_mono) |
486 apply (rule defl.principal_mono) |
487 apply (simp add: below_fin_defl_def) |
487 apply (simp add: below_fin_defl_def) |
488 apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx |
488 apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx |
489 ep_pair.finite_deflation_e_d_p [OF ep]) |
489 ep_pair.finite_deflation_e_d_p [OF ep]) |
490 apply (intro monofun_cfun below_refl) |
490 apply (intro monofun_cfun below_refl) |
491 apply (rule chainE) |
491 apply (rule chainE) |
492 apply (rule chain_lift_approx) |
492 apply (rule chain_lift_approx) |
493 apply (subst cast_sfp_principal) |
493 apply (subst cast_defl_principal) |
494 apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx |
494 apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx |
495 ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs) |
495 ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs) |
496 done |
496 done |
497 qed |
497 qed |
498 |
498 |
515 show "\<And>i. finite_deflation (ssum_approx i)" |
515 show "\<And>i. finite_deflation (ssum_approx i)" |
516 unfolding ssum_approx_def |
516 unfolding ssum_approx_def |
517 by (intro finite_deflation_ssum_map finite_deflation_udom_approx) |
517 by (intro finite_deflation_ssum_map finite_deflation_udom_approx) |
518 qed |
518 qed |
519 |
519 |
520 definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp" |
520 definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
521 where "ssum_sfp = sfp_fun2 ssum_approx ssum_map" |
521 where "ssum_defl = defl_fun2 ssum_approx ssum_map" |
522 |
522 |
523 lemma cast_ssum_sfp: |
523 lemma cast_ssum_defl: |
524 "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) = |
524 "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = |
525 udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx" |
525 udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx" |
526 unfolding ssum_sfp_def |
526 unfolding ssum_defl_def |
527 apply (rule cast_sfp_fun2 [OF ssum_approx]) |
527 apply (rule cast_defl_fun2 [OF ssum_approx]) |
528 apply (erule (1) finite_deflation_ssum_map) |
528 apply (erule (1) finite_deflation_ssum_map) |
529 done |
529 done |
530 |
530 |
531 instantiation ssum :: (bifinite, bifinite) bifinite |
531 instantiation ssum :: (bifinite, bifinite) bifinite |
532 begin |
532 begin |
536 |
536 |
537 definition |
537 definition |
538 "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx" |
538 "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx" |
539 |
539 |
540 definition |
540 definition |
541 "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
541 "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
542 |
542 |
543 instance proof |
543 instance proof |
544 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
544 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
545 unfolding emb_ssum_def prj_ssum_def |
545 unfolding emb_ssum_def prj_ssum_def |
546 using ep_pair_udom [OF ssum_approx] |
546 using ep_pair_udom [OF ssum_approx] |
547 by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj) |
547 by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj) |
548 next |
548 next |
549 show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
549 show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
550 unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp |
550 unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl |
551 by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map) |
551 by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map) |
552 qed |
552 qed |
553 |
553 |
554 end |
554 end |
555 |
555 |
556 lemma SFP_ssum: |
556 lemma DEFL_ssum: |
557 "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
557 "DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
558 by (rule sfp_ssum_def) |
558 by (rule defl_ssum_def) |
559 |
559 |
560 end |
560 end |