3 *) |
3 *) |
4 |
4 |
5 section \<open>Map functions for various types\<close> |
5 section \<open>Map functions for various types\<close> |
6 |
6 |
7 theory Map_Functions |
7 theory Map_Functions |
8 imports Deflation Sprod Ssum Sfun Up |
8 imports Deflation Sprod Ssum Sfun Up |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Map operator for continuous function space\<close> |
11 subsection \<open>Map operator for continuous function space\<close> |
12 |
12 |
13 default_sort cpo |
13 default_sort cpo |
14 |
14 |
15 definition |
15 definition cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)" |
16 cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)" |
16 where "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))" |
17 where |
|
18 "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))" |
|
19 |
17 |
20 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))" |
18 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))" |
21 unfolding cfun_map_def by simp |
19 by (simp add: cfun_map_def) |
22 |
20 |
23 lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID" |
21 lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID" |
24 unfolding cfun_eq_iff by simp |
22 by (simp add: cfun_eq_iff) |
25 |
23 |
26 lemma cfun_map_map: |
24 lemma cfun_map_map: "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) = cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
27 "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) = |
25 by (rule cfun_eqI) simp |
28 cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
29 by (rule cfun_eqI) simp |
|
30 |
26 |
31 lemma ep_pair_cfun_map: |
27 lemma ep_pair_cfun_map: |
32 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
28 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
33 shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)" |
29 shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)" |
34 proof |
30 proof |
35 interpret e1p1: ep_pair e1 p1 by fact |
31 interpret e1p1: ep_pair e1 p1 by fact |
36 interpret e2p2: ep_pair e2 p2 by fact |
32 interpret e2p2: ep_pair e2 p2 by fact |
37 fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" |
33 show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" for f |
38 by (simp add: cfun_eq_iff) |
34 by (simp add: cfun_eq_iff) |
39 fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" |
35 show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" for g |
40 apply (rule cfun_belowI, simp) |
36 apply (rule cfun_belowI, simp) |
41 apply (rule below_trans [OF e2p2.e_p_below]) |
37 apply (rule below_trans [OF e2p2.e_p_below]) |
42 apply (rule monofun_cfun_arg) |
38 apply (rule monofun_cfun_arg) |
43 apply (rule e1p1.e_p_below) |
39 apply (rule e1p1.e_p_below) |
44 done |
40 done |
95 shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
91 shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
96 proof (rule finite_deflation_intro) |
92 proof (rule finite_deflation_intro) |
97 interpret d1: finite_deflation d1 by fact |
93 interpret d1: finite_deflation d1 by fact |
98 interpret d2: finite_deflation d2 by fact |
94 interpret d2: finite_deflation d2 by fact |
99 have "deflation d1" and "deflation d2" by fact+ |
95 have "deflation d1" and "deflation d2" by fact+ |
100 thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map) |
96 then show "deflation (cfun_map\<cdot>d1\<cdot>d2)" |
|
97 by (rule deflation_cfun_map) |
101 have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))" |
98 have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))" |
102 using d1.finite_range d2.finite_range |
99 using d1.finite_range d2.finite_range |
103 by (rule finite_range_cfun_map) |
100 by (rule finite_range_cfun_map) |
104 thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
101 then show "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
105 by (rule finite_range_imp_finite_fixes) |
102 by (rule finite_range_imp_finite_fixes) |
106 qed |
103 qed |
107 |
104 |
108 text \<open>Finite deflations are compact elements of the function space\<close> |
105 text \<open>Finite deflations are compact elements of the function space\<close> |
109 |
106 |
110 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d" |
107 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d" |
111 apply (frule finite_deflation_imp_deflation) |
108 apply (frule finite_deflation_imp_deflation) |
112 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)") |
109 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)") |
113 apply (simp add: cfun_map_def deflation.idem eta_cfun) |
110 apply (simp add: cfun_map_def deflation.idem eta_cfun) |
114 apply (rule finite_deflation.compact) |
111 apply (rule finite_deflation.compact) |
115 apply (simp only: finite_deflation_cfun_map) |
112 apply (simp only: finite_deflation_cfun_map) |
116 done |
113 done |
|
114 |
117 |
115 |
118 subsection \<open>Map operator for product type\<close> |
116 subsection \<open>Map operator for product type\<close> |
119 |
117 |
120 definition |
118 definition prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd" |
121 prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd" |
119 where "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))" |
122 where |
|
123 "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))" |
|
124 |
120 |
125 lemma prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)" |
121 lemma prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)" |
126 unfolding prod_map_def by simp |
122 by (simp add: prod_map_def) |
127 |
123 |
128 lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID" |
124 lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID" |
129 unfolding cfun_eq_iff by auto |
125 by (auto simp: cfun_eq_iff) |
130 |
126 |
131 lemma prod_map_map: |
127 lemma prod_map_map: "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) = prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
132 "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
128 by (induct p) simp |
133 prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
134 by (induct p) simp |
|
135 |
129 |
136 lemma ep_pair_prod_map: |
130 lemma ep_pair_prod_map: |
137 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
131 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
138 shows "ep_pair (prod_map\<cdot>e1\<cdot>e2) (prod_map\<cdot>p1\<cdot>p2)" |
132 shows "ep_pair (prod_map\<cdot>e1\<cdot>e2) (prod_map\<cdot>p1\<cdot>p2)" |
139 proof |
133 proof |
140 interpret e1p1: ep_pair e1 p1 by fact |
134 interpret e1p1: ep_pair e1 p1 by fact |
141 interpret e2p2: ep_pair e2 p2 by fact |
135 interpret e2p2: ep_pair e2 p2 by fact |
142 fix x show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
136 show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
143 by (induct x) simp |
137 by (induct x) simp |
144 fix y show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
138 show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
145 by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) |
139 by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) |
146 qed |
140 qed |
147 |
141 |
148 lemma deflation_prod_map: |
142 lemma deflation_prod_map: |
149 assumes "deflation d1" and "deflation d2" |
143 assumes "deflation d1" and "deflation d2" |
163 shows "finite_deflation (prod_map\<cdot>d1\<cdot>d2)" |
157 shows "finite_deflation (prod_map\<cdot>d1\<cdot>d2)" |
164 proof (rule finite_deflation_intro) |
158 proof (rule finite_deflation_intro) |
165 interpret d1: finite_deflation d1 by fact |
159 interpret d1: finite_deflation d1 by fact |
166 interpret d2: finite_deflation d2 by fact |
160 interpret d2: finite_deflation d2 by fact |
167 have "deflation d1" and "deflation d2" by fact+ |
161 have "deflation d1" and "deflation d2" by fact+ |
168 thus "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map) |
162 then show "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map) |
169 have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}" |
163 have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}" |
170 by clarsimp |
164 by auto |
171 thus "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}" |
165 then show "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}" |
172 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
166 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
173 qed |
167 qed |
174 |
168 |
|
169 |
175 subsection \<open>Map function for lifted cpo\<close> |
170 subsection \<open>Map function for lifted cpo\<close> |
176 |
171 |
177 definition |
172 definition u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u" |
178 u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u" |
173 where "u_map = (\<Lambda> f. fup\<cdot>(up oo f))" |
179 where |
|
180 "u_map = (\<Lambda> f. fup\<cdot>(up oo f))" |
|
181 |
174 |
182 lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>" |
175 lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>" |
183 unfolding u_map_def by simp |
176 by (simp add: u_map_def) |
184 |
177 |
185 lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)" |
178 lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)" |
186 unfolding u_map_def by simp |
179 by (simp add: u_map_def) |
187 |
180 |
188 lemma u_map_ID: "u_map\<cdot>ID = ID" |
181 lemma u_map_ID: "u_map\<cdot>ID = ID" |
189 unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun) |
182 by (simp add: u_map_def cfun_eq_iff eta_cfun) |
190 |
183 |
191 lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p" |
184 lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p" |
192 by (induct p) simp_all |
185 by (induct p) simp_all |
193 |
186 |
194 lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g" |
187 lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g" |
195 by (simp add: cfcomp1 u_map_map eta_cfun) |
188 by (simp add: cfcomp1 u_map_map eta_cfun) |
196 |
189 |
197 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)" |
190 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)" |
198 apply standard |
191 apply standard |
199 apply (case_tac x, simp, simp add: ep_pair.e_inverse) |
192 subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse) |
200 apply (case_tac y, simp, simp add: ep_pair.e_p_below) |
193 subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below) |
201 done |
194 done |
202 |
195 |
203 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)" |
196 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)" |
204 apply standard |
197 apply standard |
205 apply (case_tac x, simp, simp add: deflation.idem) |
198 subgoal for x by (cases x, simp, simp add: deflation.idem) |
206 apply (case_tac x, simp, simp add: deflation.below) |
199 subgoal for x by (cases x, simp, simp add: deflation.below) |
207 done |
200 done |
208 |
201 |
209 lemma finite_deflation_u_map: |
202 lemma finite_deflation_u_map: |
210 assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)" |
203 assumes "finite_deflation d" |
|
204 shows "finite_deflation (u_map\<cdot>d)" |
211 proof (rule finite_deflation_intro) |
205 proof (rule finite_deflation_intro) |
212 interpret d: finite_deflation d by fact |
206 interpret d: finite_deflation d by fact |
213 have "deflation d" by fact |
207 have "deflation d" by fact |
214 thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map) |
208 then show "deflation (u_map\<cdot>d)" |
|
209 by (rule deflation_u_map) |
215 have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})" |
210 have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})" |
216 by (rule subsetI, case_tac x, simp_all) |
211 by (rule subsetI, case_tac x, simp_all) |
217 thus "finite {x. u_map\<cdot>d\<cdot>x = x}" |
212 then show "finite {x. u_map\<cdot>d\<cdot>x = x}" |
218 by (rule finite_subset, simp add: d.finite_fixes) |
213 by (rule finite_subset) (simp add: d.finite_fixes) |
219 qed |
214 qed |
|
215 |
220 |
216 |
221 subsection \<open>Map function for strict products\<close> |
217 subsection \<open>Map function for strict products\<close> |
222 |
218 |
223 default_sort pcpo |
219 default_sort pcpo |
224 |
220 |
225 definition |
221 definition sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd" |
226 sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd" |
222 where "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))" |
227 where |
|
228 "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))" |
|
229 |
223 |
230 lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
224 lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
231 unfolding sprod_map_def by simp |
225 by (simp add: sprod_map_def) |
232 |
226 |
233 lemma sprod_map_spair [simp]: |
227 lemma sprod_map_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
234 "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
228 by (simp add: sprod_map_def) |
235 by (simp add: sprod_map_def) |
229 |
236 |
230 lemma sprod_map_spair': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
237 lemma sprod_map_spair': |
231 by (cases "x = \<bottom> \<or> y = \<bottom>") auto |
238 "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
|
239 by (cases "x = \<bottom> \<or> y = \<bottom>") auto |
|
240 |
232 |
241 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID" |
233 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID" |
242 unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun) |
234 by (simp add: sprod_map_def cfun_eq_iff eta_cfun) |
243 |
235 |
244 lemma sprod_map_map: |
236 lemma sprod_map_map: |
245 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
237 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
246 sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
238 sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
247 sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
239 sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
248 apply (induct p, simp) |
240 apply (induct p) |
249 apply (case_tac "f2\<cdot>x = \<bottom>", simp) |
241 apply simp |
250 apply (case_tac "g2\<cdot>y = \<bottom>", simp) |
242 apply (case_tac "f2\<cdot>x = \<bottom>", simp) |
251 apply simp |
243 apply (case_tac "g2\<cdot>y = \<bottom>", simp) |
252 done |
244 apply simp |
|
245 done |
253 |
246 |
254 lemma ep_pair_sprod_map: |
247 lemma ep_pair_sprod_map: |
255 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
248 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
256 shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
249 shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
257 proof |
250 proof |
258 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
251 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
259 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
252 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
260 fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
253 show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
261 by (induct x) simp_all |
254 by (induct x) simp_all |
262 fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
255 show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
263 apply (induct y, simp) |
256 apply (induct y) |
|
257 apply simp |
264 apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp) |
258 apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp) |
265 apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
259 apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
266 done |
260 done |
267 qed |
261 qed |
268 |
262 |
289 shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
283 shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
290 proof (rule finite_deflation_intro) |
284 proof (rule finite_deflation_intro) |
291 interpret d1: finite_deflation d1 by fact |
285 interpret d1: finite_deflation d1 by fact |
292 interpret d2: finite_deflation d2 by fact |
286 interpret d2: finite_deflation d2 by fact |
293 have "deflation d1" and "deflation d2" by fact+ |
287 have "deflation d1" and "deflation d2" by fact+ |
294 thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map) |
288 then show "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
295 have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom> |
289 by (rule deflation_sprod_map) |
296 ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))" |
290 have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> |
|
291 insert \<bottom> ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))" |
297 by (rule subsetI, case_tac x, auto simp add: spair_eq_iff) |
292 by (rule subsetI, case_tac x, auto simp add: spair_eq_iff) |
298 thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
293 then show "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
299 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
294 by (rule finite_subset) (simp add: d1.finite_fixes d2.finite_fixes) |
300 qed |
295 qed |
|
296 |
301 |
297 |
302 subsection \<open>Map function for strict sums\<close> |
298 subsection \<open>Map function for strict sums\<close> |
303 |
299 |
304 definition |
300 definition ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd" |
305 ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd" |
301 where "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))" |
306 where |
|
307 "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))" |
|
308 |
302 |
309 lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>" |
303 lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>" |
310 unfolding ssum_map_def by simp |
304 by (simp add: ssum_map_def) |
311 |
305 |
312 lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
306 lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
313 unfolding ssum_map_def by simp |
307 by (simp add: ssum_map_def) |
314 |
308 |
315 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
309 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
316 unfolding ssum_map_def by simp |
310 by (simp add: ssum_map_def) |
317 |
311 |
318 lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
312 lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
319 by (cases "x = \<bottom>") simp_all |
313 by (cases "x = \<bottom>") simp_all |
320 |
314 |
321 lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
315 lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
322 by (cases "x = \<bottom>") simp_all |
316 by (cases "x = \<bottom>") simp_all |
323 |
317 |
324 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID" |
318 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID" |
325 unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun) |
319 by (simp add: ssum_map_def cfun_eq_iff eta_cfun) |
326 |
320 |
327 lemma ssum_map_map: |
321 lemma ssum_map_map: |
328 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
322 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
329 ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) = |
323 ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) = |
330 ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
324 ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
331 apply (induct p, simp) |
325 apply (induct p) |
332 apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp) |
326 apply simp |
333 apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp) |
327 apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp) |
334 done |
328 apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp) |
|
329 done |
335 |
330 |
336 lemma ep_pair_ssum_map: |
331 lemma ep_pair_ssum_map: |
337 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
332 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
338 shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)" |
333 shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)" |
339 proof |
334 proof |
340 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
335 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
341 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
336 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
342 fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
337 show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
343 by (induct x) simp_all |
338 by (induct x) simp_all |
344 fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
339 show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
345 apply (induct y, simp) |
340 apply (induct y) |
346 apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below) |
341 apply simp |
|
342 apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below) |
347 apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below) |
343 apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below) |
348 done |
344 done |
349 qed |
345 qed |
350 |
346 |
351 lemma deflation_ssum_map: |
347 lemma deflation_ssum_map: |
372 shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)" |
368 shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)" |
373 proof (rule finite_deflation_intro) |
369 proof (rule finite_deflation_intro) |
374 interpret d1: finite_deflation d1 by fact |
370 interpret d1: finite_deflation d1 by fact |
375 interpret d2: finite_deflation d2 by fact |
371 interpret d2: finite_deflation d2 by fact |
376 have "deflation d1" and "deflation d2" by fact+ |
372 have "deflation d1" and "deflation d2" by fact+ |
377 thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map) |
373 then show "deflation (ssum_map\<cdot>d1\<cdot>d2)" |
|
374 by (rule deflation_ssum_map) |
378 have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> |
375 have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> |
379 (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union> |
376 (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union> |
380 (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}" |
377 (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}" |
381 by (rule subsetI, case_tac x, simp_all) |
378 by (rule subsetI, case_tac x, simp_all) |
382 thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
379 then show "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
383 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
380 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
384 qed |
381 qed |
385 |
382 |
|
383 |
386 subsection \<open>Map operator for strict function space\<close> |
384 subsection \<open>Map operator for strict function space\<close> |
387 |
385 |
388 definition |
386 definition sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)" |
389 sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)" |
387 where "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)" |
390 where |
|
391 "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)" |
|
392 |
388 |
393 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID" |
389 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID" |
394 unfolding sfun_map_def |
390 by (simp add: sfun_map_def cfun_map_ID cfun_eq_iff) |
395 by (simp add: cfun_map_ID cfun_eq_iff) |
|
396 |
391 |
397 lemma sfun_map_map: |
392 lemma sfun_map_map: |
398 assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows |
393 assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" |
399 "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) = |
394 shows "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) = |
400 sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
395 sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
401 unfolding sfun_map_def |
396 by (simp add: sfun_map_def cfun_eq_iff strictify_cancel assms cfun_map_map) |
402 by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map) |
|
403 |
397 |
404 lemma ep_pair_sfun_map: |
398 lemma ep_pair_sfun_map: |
405 assumes 1: "ep_pair e1 p1" |
399 assumes 1: "ep_pair e1 p1" |
406 assumes 2: "ep_pair e2 p2" |
400 assumes 2: "ep_pair e2 p2" |
407 shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)" |
401 shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)" |
408 proof |
402 proof |
409 interpret e1p1: pcpo_ep_pair e1 p1 |
403 interpret e1p1: pcpo_ep_pair e1 p1 |
410 unfolding pcpo_ep_pair_def by fact |
404 unfolding pcpo_ep_pair_def by fact |
411 interpret e2p2: pcpo_ep_pair e2 p2 |
405 interpret e2p2: pcpo_ep_pair e2 p2 |
412 unfolding pcpo_ep_pair_def by fact |
406 unfolding pcpo_ep_pair_def by fact |
413 fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" |
407 show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" for f |
414 unfolding sfun_map_def |
408 unfolding sfun_map_def |
415 apply (simp add: sfun_eq_iff strictify_cancel) |
409 apply (simp add: sfun_eq_iff strictify_cancel) |
416 apply (rule ep_pair.e_inverse) |
410 apply (rule ep_pair.e_inverse) |
417 apply (rule ep_pair_cfun_map [OF 1 2]) |
411 apply (rule ep_pair_cfun_map [OF 1 2]) |
418 done |
412 done |
419 fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" |
413 show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" for g |
420 unfolding sfun_map_def |
414 unfolding sfun_map_def |
421 apply (simp add: sfun_below_iff strictify_cancel) |
415 apply (simp add: sfun_below_iff strictify_cancel) |
422 apply (rule ep_pair.e_p_below) |
416 apply (rule ep_pair.e_p_below) |
423 apply (rule ep_pair_cfun_map [OF 1 2]) |
417 apply (rule ep_pair_cfun_map [OF 1 2]) |
424 done |
418 done |
426 |
420 |
427 lemma deflation_sfun_map: |
421 lemma deflation_sfun_map: |
428 assumes 1: "deflation d1" |
422 assumes 1: "deflation d1" |
429 assumes 2: "deflation d2" |
423 assumes 2: "deflation d2" |
430 shows "deflation (sfun_map\<cdot>d1\<cdot>d2)" |
424 shows "deflation (sfun_map\<cdot>d1\<cdot>d2)" |
431 apply (simp add: sfun_map_def) |
425 apply (simp add: sfun_map_def) |
432 apply (rule deflation.intro) |
426 apply (rule deflation.intro) |
433 apply simp |
427 apply simp |
434 apply (subst strictify_cancel) |
428 apply (subst strictify_cancel) |
435 apply (simp add: cfun_map_def deflation_strict 1 2) |
429 apply (simp add: cfun_map_def deflation_strict 1 2) |
436 apply (simp add: cfun_map_def deflation.idem 1 2) |
430 apply (simp add: cfun_map_def deflation.idem 1 2) |
437 apply (simp add: sfun_below_iff) |
431 apply (simp add: sfun_below_iff) |
438 apply (subst strictify_cancel) |
432 apply (subst strictify_cancel) |
439 apply (simp add: cfun_map_def deflation_strict 1 2) |
433 apply (simp add: cfun_map_def deflation_strict 1 2) |
440 apply (rule deflation.below) |
434 apply (rule deflation.below) |
441 apply (rule deflation_cfun_map [OF 1 2]) |
435 apply (rule deflation_cfun_map [OF 1 2]) |
442 done |
436 done |
443 |
437 |
444 lemma finite_deflation_sfun_map: |
438 lemma finite_deflation_sfun_map: |
445 assumes 1: "finite_deflation d1" |
439 assumes "finite_deflation d1" |
446 assumes 2: "finite_deflation d2" |
440 and "finite_deflation d2" |
447 shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)" |
441 shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)" |
448 proof (intro finite_deflation_intro) |
442 proof (intro finite_deflation_intro) |
449 interpret d1: finite_deflation d1 by fact |
443 interpret d1: finite_deflation d1 by fact |
450 interpret d2: finite_deflation d2 by fact |
444 interpret d2: finite_deflation d2 by fact |
451 have "deflation d1" and "deflation d2" by fact+ |
445 have "deflation d1" and "deflation d2" by fact+ |
452 thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map) |
446 then show "deflation (sfun_map\<cdot>d1\<cdot>d2)" |
453 from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
447 by (rule deflation_sfun_map) |
|
448 from assms have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
454 by (rule finite_deflation_cfun_map) |
449 by (rule finite_deflation_cfun_map) |
455 then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
450 then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
456 by (rule finite_deflation.finite_fixes) |
451 by (rule finite_deflation.finite_fixes) |
457 moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)" |
452 moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)" |
458 by (rule inj_onI, simp add: sfun_eq_iff) |
453 by (rule inj_onI) (simp add: sfun_eq_iff) |
459 ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})" |
454 ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})" |
460 by (rule finite_vimageI) |
455 by (rule finite_vimageI) |
461 then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
456 with \<open>deflation d1\<close> \<open>deflation d2\<close> show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
462 unfolding sfun_map_def sfun_eq_iff |
457 by (simp add: sfun_map_def sfun_eq_iff strictify_cancel deflation_strict) |
463 by (simp add: strictify_cancel |
|
464 deflation_strict \<open>deflation d1\<close> \<open>deflation d2\<close>) |
|
465 qed |
458 qed |
466 |
459 |
467 end |
460 end |