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