1(* Title: HOL/HOLCF/Representable.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Representable domains\<close> 6 7theory Representable 8imports Algebraic Map_Functions "HOL-Library.Countable" 9begin 10 11default_sort cpo 12 13subsection \<open>Class of representable domains\<close> 14 15text \<open> 16 We define a ``domain'' as a pcpo that is isomorphic to some 17 algebraic deflation over the universal domain; this is equivalent 18 to being omega-bifinite. 19 20 A predomain is a cpo that, when lifted, becomes a domain. 21 Predomains are represented by deflations over a lifted universal 22 domain type. 23\<close> 24 25class predomain_syn = cpo + 26 fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>" 27 fixes liftprj :: "udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" 28 fixes liftdefl :: "'a itself \<Rightarrow> udom u defl" 29 30class predomain = predomain_syn + 31 assumes predomain_ep: "ep_pair liftemb liftprj" 32 assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj" 33 34syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))") 35translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)" 36 37definition liftdefl_of :: "udom defl \<rightarrow> udom u defl" 38 where "liftdefl_of = defl_fun1 ID ID u_map" 39 40lemma cast_liftdefl_of: "cast\<cdot>(liftdefl_of\<cdot>t) = u_map\<cdot>(cast\<cdot>t)" 41by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map) 42 43class "domain" = predomain_syn + pcpo + 44 fixes emb :: "'a \<rightarrow> udom" 45 fixes prj :: "udom \<rightarrow> 'a" 46 fixes defl :: "'a itself \<Rightarrow> udom defl" 47 assumes ep_pair_emb_prj: "ep_pair emb prj" 48 assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj" 49 assumes liftemb_eq: "liftemb = u_map\<cdot>emb" 50 assumes liftprj_eq: "liftprj = u_map\<cdot>prj" 51 assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))" 52 53syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))") 54translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)" 55 56instance "domain" \<subseteq> predomain 57proof 58 show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)" 59 unfolding liftemb_eq liftprj_eq 60 by (intro ep_pair_u_map ep_pair_emb_prj) 61 show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)" 62 unfolding liftemb_eq liftprj_eq liftdefl_eq 63 by (simp add: cast_liftdefl_of cast_DEFL u_map_oo) 64qed 65 66text \<open> 67 Constants \<^const>\<open>liftemb\<close> and \<^const>\<open>liftprj\<close> imply class predomain. 68\<close> 69 70setup \<open> 71 fold Sign.add_const_constraint 72 [(\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::predomain u \<rightarrow> udom u\<close>), 73 (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>), 74 (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::predomain itself \<Rightarrow> udom u defl\<close>)] 75\<close> 76 77interpretation predomain: pcpo_ep_pair liftemb liftprj 78 unfolding pcpo_ep_pair_def by (rule predomain_ep) 79 80interpretation "domain": pcpo_ep_pair emb prj 81 unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj) 82 83lemmas emb_inverse = domain.e_inverse 84lemmas emb_prj_below = domain.e_p_below 85lemmas emb_eq_iff = domain.e_eq_iff 86lemmas emb_strict = domain.e_strict 87lemmas prj_strict = domain.p_strict 88 89subsection \<open>Domains are bifinite\<close> 90 91lemma approx_chain_ep_cast: 92 assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)" 93 assumes cast_t: "cast\<cdot>t = e oo p" 94 shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a" 95proof - 96 interpret ep_pair e p by fact 97 obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" 98 and t: "t = (\<Squnion>i. defl_principal (Y i))" 99 by (rule defl.obtain_principal_chain) 100 define approx where "approx i = (p oo cast\<cdot>(defl_principal (Y i)) oo e)" for i 101 have "approx_chain approx" 102 proof (rule approx_chain.intro) 103 show "chain (\<lambda>i. approx i)" 104 unfolding approx_def by (simp add: Y) 105 show "(\<Squnion>i. approx i) = ID" 106 unfolding approx_def 107 by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff) 108 show "\<And>i. finite_deflation (approx i)" 109 unfolding approx_def 110 apply (rule finite_deflation_p_d_e) 111 apply (rule finite_deflation_cast) 112 apply (rule defl.compact_principal) 113 apply (rule below_trans [OF monofun_cfun_fun]) 114 apply (rule is_ub_thelub, simp add: Y) 115 apply (simp add: lub_distribs Y t [symmetric] cast_t) 116 done 117 qed 118 thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI) 119qed 120 121instance "domain" \<subseteq> bifinite 122by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL]) 123 124instance predomain \<subseteq> profinite 125by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl]) 126 127subsection \<open>Universal domain ep-pairs\<close> 128 129definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))" 130definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))" 131 132definition "prod_emb = udom_emb (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 133definition "prod_prj = udom_prj (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 134 135definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 136definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 137 138definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 139definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 140 141definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 142definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" 143 144lemma ep_pair_u: "ep_pair u_emb u_prj" 145 unfolding u_emb_def u_prj_def 146 by (simp add: ep_pair_udom approx_chain_u_map) 147 148lemma ep_pair_prod: "ep_pair prod_emb prod_prj" 149 unfolding prod_emb_def prod_prj_def 150 by (simp add: ep_pair_udom approx_chain_prod_map) 151 152lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj" 153 unfolding sprod_emb_def sprod_prj_def 154 by (simp add: ep_pair_udom approx_chain_sprod_map) 155 156lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj" 157 unfolding ssum_emb_def ssum_prj_def 158 by (simp add: ep_pair_udom approx_chain_ssum_map) 159 160lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj" 161 unfolding sfun_emb_def sfun_prj_def 162 by (simp add: ep_pair_udom approx_chain_sfun_map) 163 164subsection \<open>Type combinators\<close> 165 166definition u_defl :: "udom defl \<rightarrow> udom defl" 167 where "u_defl = defl_fun1 u_emb u_prj u_map" 168 169definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" 170 where "prod_defl = defl_fun2 prod_emb prod_prj prod_map" 171 172definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" 173 where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map" 174 175definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" 176where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map" 177 178definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl" 179 where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map" 180 181lemma cast_u_defl: 182 "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj" 183using ep_pair_u finite_deflation_u_map 184unfolding u_defl_def by (rule cast_defl_fun1) 185 186lemma cast_prod_defl: 187 "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = 188 prod_emb oo prod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj" 189using ep_pair_prod finite_deflation_prod_map 190unfolding prod_defl_def by (rule cast_defl_fun2) 191 192lemma cast_sprod_defl: 193 "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = 194 sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj" 195using ep_pair_sprod finite_deflation_sprod_map 196unfolding sprod_defl_def by (rule cast_defl_fun2) 197 198lemma cast_ssum_defl: 199 "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = 200 ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj" 201using ep_pair_ssum finite_deflation_ssum_map 202unfolding ssum_defl_def by (rule cast_defl_fun2) 203 204lemma cast_sfun_defl: 205 "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) = 206 sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj" 207using ep_pair_sfun finite_deflation_sfun_map 208unfolding sfun_defl_def by (rule cast_defl_fun2) 209 210text \<open>Special deflation combinator for unpointed types.\<close> 211 212definition u_liftdefl :: "udom u defl \<rightarrow> udom defl" 213 where "u_liftdefl = defl_fun1 u_emb u_prj ID" 214 215lemma cast_u_liftdefl: 216 "cast\<cdot>(u_liftdefl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj" 217unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u) 218 219lemma u_liftdefl_liftdefl_of: 220 "u_liftdefl\<cdot>(liftdefl_of\<cdot>A) = u_defl\<cdot>A" 221by (rule cast_eq_imp_eq) 222 (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl) 223 224subsection \<open>Class instance proofs\<close> 225 226subsubsection \<open>Universal domain\<close> 227 228instantiation udom :: "domain" 229begin 230 231definition [simp]: 232 "emb = (ID :: udom \<rightarrow> udom)" 233 234definition [simp]: 235 "prj = (ID :: udom \<rightarrow> udom)" 236 237definition 238 "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))" 239 240definition 241 "(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb" 242 243definition 244 "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj" 245 246definition 247 "liftdefl (t::udom itself) = liftdefl_of\<cdot>DEFL(udom)" 248 249instance proof 250 show "ep_pair emb (prj :: udom \<rightarrow> udom)" 251 by (simp add: ep_pair.intro) 252 show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)" 253 unfolding defl_udom_def 254 apply (subst contlub_cfun_arg) 255 apply (rule chainI) 256 apply (rule defl.principal_mono) 257 apply (simp add: below_fin_defl_def) 258 apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) 259 apply (rule chainE) 260 apply (rule chain_udom_approx) 261 apply (subst cast_defl_principal) 262 apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) 263 done 264qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+ 265 266end 267 268subsubsection \<open>Lifted cpo\<close> 269 270instantiation u :: (predomain) "domain" 271begin 272 273definition 274 "emb = u_emb oo liftemb" 275 276definition 277 "prj = liftprj oo u_prj" 278 279definition 280 "defl (t::'a u itself) = u_liftdefl\<cdot>LIFTDEFL('a)" 281 282definition 283 "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb" 284 285definition 286 "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj" 287 288definition 289 "liftdefl (t::'a u itself) = liftdefl_of\<cdot>DEFL('a u)" 290 291instance proof 292 show "ep_pair emb (prj :: udom \<rightarrow> 'a u)" 293 unfolding emb_u_def prj_u_def 294 by (intro ep_pair_comp ep_pair_u predomain_ep) 295 show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)" 296 unfolding emb_u_def prj_u_def defl_u_def 297 by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo) 298qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+ 299 300end 301 302lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)" 303by (rule defl_u_def) 304 305subsubsection \<open>Strict function space\<close> 306 307instantiation sfun :: ("domain", "domain") "domain" 308begin 309 310definition 311 "emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb" 312 313definition 314 "prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj" 315 316definition 317 "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 318 319definition 320 "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" 321 322definition 323 "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj" 324 325definition 326 "liftdefl (t::('a \<rightarrow>! 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow>! 'b)" 327 328instance proof 329 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" 330 unfolding emb_sfun_def prj_sfun_def 331 by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj) 332 show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)" 333 unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl 334 by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map) 335qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+ 336 337end 338 339lemma DEFL_sfun: 340 "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 341by (rule defl_sfun_def) 342 343subsubsection \<open>Continuous function space\<close> 344 345instantiation cfun :: (predomain, "domain") "domain" 346begin 347 348definition 349 "emb = emb oo encode_cfun" 350 351definition 352 "prj = decode_cfun oo prj" 353 354definition 355 "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)" 356 357definition 358 "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" 359 360definition 361 "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj" 362 363definition 364 "liftdefl (t::('a \<rightarrow> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow> 'b)" 365 366instance proof 367 have "ep_pair encode_cfun decode_cfun" 368 by (rule ep_pair.intro, simp_all) 369 thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" 370 unfolding emb_cfun_def prj_cfun_def 371 using ep_pair_emb_prj by (rule ep_pair_comp) 372 show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" 373 unfolding emb_cfun_def prj_cfun_def defl_cfun_def 374 by (simp add: cast_DEFL cfcomp1) 375qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+ 376 377end 378 379lemma DEFL_cfun: 380 "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)" 381by (rule defl_cfun_def) 382 383subsubsection \<open>Strict product\<close> 384 385instantiation sprod :: ("domain", "domain") "domain" 386begin 387 388definition 389 "emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb" 390 391definition 392 "prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj" 393 394definition 395 "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 396 397definition 398 "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" 399 400definition 401 "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj" 402 403definition 404 "liftdefl (t::('a \<otimes> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<otimes> 'b)" 405 406instance proof 407 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)" 408 unfolding emb_sprod_def prj_sprod_def 409 by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj) 410 show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)" 411 unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl 412 by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map) 413qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+ 414 415end 416 417lemma DEFL_sprod: 418 "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 419by (rule defl_sprod_def) 420 421subsubsection \<open>Cartesian product\<close> 422 423definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl" 424 where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u) 425 (encode_prod_u oo u_map\<cdot>prod_prj) sprod_map" 426 427lemma cast_prod_liftdefl: 428 "cast\<cdot>(prod_liftdefl\<cdot>a\<cdot>b) = 429 (u_map\<cdot>prod_emb oo decode_prod_u) oo sprod_map\<cdot>(cast\<cdot>a)\<cdot>(cast\<cdot>b) oo 430 (encode_prod_u oo u_map\<cdot>prod_prj)" 431unfolding prod_liftdefl_def 432apply (rule cast_defl_fun2) 433apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod) 434apply (simp add: ep_pair.intro) 435apply (erule (1) finite_deflation_sprod_map) 436done 437 438instantiation prod :: (predomain, predomain) predomain 439begin 440 441definition 442 "liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo 443 (sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)" 444 445definition 446 "liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo 447 (encode_prod_u oo u_map\<cdot>prod_prj)" 448 449definition 450 "liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" 451 452instance proof 453 show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)" 454 unfolding liftemb_prod_def liftprj_prod_def 455 by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map 456 ep_pair_prod predomain_ep, simp_all add: ep_pair.intro) 457 show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)" 458 unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def 459 by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map) 460qed 461 462end 463 464instantiation prod :: ("domain", "domain") "domain" 465begin 466 467definition 468 "emb = prod_emb oo prod_map\<cdot>emb\<cdot>emb" 469 470definition 471 "prj = prod_map\<cdot>prj\<cdot>prj oo prod_prj" 472 473definition 474 "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 475 476instance proof 477 show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)" 478 unfolding emb_prod_def prj_prod_def 479 by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj) 480 show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)" 481 unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl 482 by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map) 483 show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)" 484 unfolding emb_prod_def liftemb_prod_def liftemb_eq 485 unfolding encode_prod_u_def decode_prod_u_def 486 by (rule cfun_eqI, case_tac x, simp, clarsimp) 487 show 4: "liftprj = u_map\<cdot>(prj :: udom \<rightarrow> 'a \<times> 'b)" 488 unfolding prj_prod_def liftprj_prod_def liftprj_eq 489 unfolding encode_prod_u_def decode_prod_u_def 490 apply (rule cfun_eqI, case_tac x, simp) 491 apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp) 492 done 493 show 5: "LIFTDEFL('a \<times> 'b) = liftdefl_of\<cdot>DEFL('a \<times> 'b)" 494 by (rule cast_eq_imp_eq) 495 (simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo) 496qed 497 498end 499 500lemma DEFL_prod: 501 "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 502by (rule defl_prod_def) 503 504lemma LIFTDEFL_prod: 505 "LIFTDEFL('a::predomain \<times> 'b::predomain) = 506 prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)" 507by (rule liftdefl_prod_def) 508 509subsubsection \<open>Unit type\<close> 510 511instantiation unit :: "domain" 512begin 513 514definition 515 "emb = (\<bottom> :: unit \<rightarrow> udom)" 516 517definition 518 "prj = (\<bottom> :: udom \<rightarrow> unit)" 519 520definition 521 "defl (t::unit itself) = \<bottom>" 522 523definition 524 "(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb" 525 526definition 527 "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj" 528 529definition 530 "liftdefl (t::unit itself) = liftdefl_of\<cdot>DEFL(unit)" 531 532instance proof 533 show "ep_pair emb (prj :: udom \<rightarrow> unit)" 534 unfolding emb_unit_def prj_unit_def 535 by (simp add: ep_pair.intro) 536 show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)" 537 unfolding emb_unit_def prj_unit_def defl_unit_def by simp 538qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+ 539 540end 541 542subsubsection \<open>Discrete cpo\<close> 543 544instantiation discr :: (countable) predomain 545begin 546 547definition 548 "(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx" 549 550definition 551 "(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID" 552 553definition 554 "liftdefl (t::'a discr itself) = 555 (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))" 556 557instance proof 558 show 1: "ep_pair liftemb (liftprj :: udom u \<rightarrow> 'a discr u)" 559 unfolding liftemb_discr_def liftprj_discr_def 560 apply (intro ep_pair_comp ep_pair_udom [OF discr_approx]) 561 apply (rule ep_pair.intro) 562 apply (simp add: strictify_conv_if) 563 apply (case_tac y, simp, simp add: strictify_conv_if) 564 done 565 show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \<rightarrow> 'a discr u)" 566 unfolding liftdefl_discr_def 567 apply (subst contlub_cfun_arg) 568 apply (rule chainI) 569 apply (rule defl.principal_mono) 570 apply (simp add: below_fin_defl_def) 571 apply (simp add: Abs_fin_defl_inverse 572 ep_pair.finite_deflation_e_d_p [OF 1] 573 approx_chain.finite_deflation_approx [OF discr_approx]) 574 apply (intro monofun_cfun below_refl) 575 apply (rule chainE) 576 apply (rule chain_discr_approx) 577 apply (subst cast_defl_principal) 578 apply (simp add: Abs_fin_defl_inverse 579 ep_pair.finite_deflation_e_d_p [OF 1] 580 approx_chain.finite_deflation_approx [OF discr_approx]) 581 apply (simp add: lub_distribs) 582 done 583qed 584 585end 586 587subsubsection \<open>Strict sum\<close> 588 589instantiation ssum :: ("domain", "domain") "domain" 590begin 591 592definition 593 "emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb" 594 595definition 596 "prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj" 597 598definition 599 "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 600 601definition 602 "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb" 603 604definition 605 "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj" 606 607definition 608 "liftdefl (t::('a \<oplus> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<oplus> 'b)" 609 610instance proof 611 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)" 612 unfolding emb_ssum_def prj_ssum_def 613 by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj) 614 show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)" 615 unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl 616 by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map) 617qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+ 618 619end 620 621lemma DEFL_ssum: 622 "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" 623by (rule defl_ssum_def) 624 625subsubsection \<open>Lifted HOL type\<close> 626 627instantiation lift :: (countable) "domain" 628begin 629 630definition 631 "emb = emb oo (\<Lambda> x. Rep_lift x)" 632 633definition 634 "prj = (\<Lambda> y. Abs_lift y) oo prj" 635 636definition 637 "defl (t::'a lift itself) = DEFL('a discr u)" 638 639definition 640 "(liftemb :: 'a lift u \<rightarrow> udom u) = u_map\<cdot>emb" 641 642definition 643 "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj" 644 645definition 646 "liftdefl (t::'a lift itself) = liftdefl_of\<cdot>DEFL('a lift)" 647 648instance proof 649 note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse 650 have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)" 651 by (simp add: ep_pair_def) 652 thus "ep_pair emb (prj :: udom \<rightarrow> 'a lift)" 653 unfolding emb_lift_def prj_lift_def 654 using ep_pair_emb_prj by (rule ep_pair_comp) 655 show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)" 656 unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL 657 by (simp add: cfcomp1) 658qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+ 659 660end 661 662end 663