src/HOL/HOLCF/Representable.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/HOLCF/Representable.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Representable domains\<close>
     6 
     7 theory Representable
     8 imports Algebraic Map_Functions "HOL-Library.Countable"
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection \<open>Class of representable domains\<close>
    14 
    15 text \<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 
    25 class 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 
    30 class predomain = predomain_syn +
    31   assumes predomain_ep: "ep_pair liftemb liftprj"
    32   assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
    33 
    34 syntax "_LIFTDEFL" :: "type \<Rightarrow> logic"  ("(1LIFTDEFL/(1'(_')))")
    35 translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
    36 
    37 definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
    38   where "liftdefl_of = defl_fun1 ID ID u_map"
    39 
    40 lemma cast_liftdefl_of: "cast\<cdot>(liftdefl_of\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
    41 by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
    42 
    43 class "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 
    53 syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
    54 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
    55 
    56 instance "domain" \<subseteq> predomain
    57 proof
    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)
    64 qed
    65 
    66 text \<open>
    67   Constants @{const liftemb} and @{const liftprj} imply class predomain.
    68 \<close>
    69 
    70 setup \<open>
    71   fold Sign.add_const_constraint
    72   [(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
    73    (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}),
    74    (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})]
    75 \<close>
    76 
    77 interpretation predomain: pcpo_ep_pair liftemb liftprj
    78   unfolding pcpo_ep_pair_def by (rule predomain_ep)
    79 
    80 interpretation "domain": pcpo_ep_pair emb prj
    81   unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj)
    82 
    83 lemmas emb_inverse = domain.e_inverse
    84 lemmas emb_prj_below = domain.e_p_below
    85 lemmas emb_eq_iff = domain.e_eq_iff
    86 lemmas emb_strict = domain.e_strict
    87 lemmas prj_strict = domain.p_strict
    88 
    89 subsection \<open>Domains are bifinite\<close>
    90 
    91 lemma 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"
    95 proof -
    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)
   119 qed
   120 
   121 instance "domain" \<subseteq> bifinite
   122 by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
   123 
   124 instance predomain \<subseteq> profinite
   125 by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
   126 
   127 subsection \<open>Universal domain ep-pairs\<close>
   128 
   129 definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
   130 definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
   131 
   132 definition "prod_emb = udom_emb (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   133 definition "prod_prj = udom_prj (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   134 
   135 definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   136 definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   137 
   138 definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   139 definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   140 
   141 definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   142 definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   143 
   144 lemma 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 
   148 lemma 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 
   152 lemma 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 
   156 lemma 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 
   160 lemma 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 
   164 subsection \<open>Type combinators\<close>
   165 
   166 definition u_defl :: "udom defl \<rightarrow> udom defl"
   167   where "u_defl = defl_fun1 u_emb u_prj u_map"
   168 
   169 definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   170   where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
   171 
   172 definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   173   where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
   174 
   175 definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   176 where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"
   177 
   178 definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   179   where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
   180 
   181 lemma cast_u_defl:
   182   "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj"
   183 using ep_pair_u finite_deflation_u_map
   184 unfolding u_defl_def by (rule cast_defl_fun1)
   185 
   186 lemma 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"
   189 using ep_pair_prod finite_deflation_prod_map
   190 unfolding prod_defl_def by (rule cast_defl_fun2)
   191 
   192 lemma 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"
   195 using ep_pair_sprod finite_deflation_sprod_map
   196 unfolding sprod_defl_def by (rule cast_defl_fun2)
   197 
   198 lemma 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"
   201 using ep_pair_ssum finite_deflation_ssum_map
   202 unfolding ssum_defl_def by (rule cast_defl_fun2)
   203 
   204 lemma 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"
   207 using ep_pair_sfun finite_deflation_sfun_map
   208 unfolding sfun_defl_def by (rule cast_defl_fun2)
   209 
   210 text \<open>Special deflation combinator for unpointed types.\<close>
   211 
   212 definition u_liftdefl :: "udom u defl \<rightarrow> udom defl"
   213   where "u_liftdefl = defl_fun1 u_emb u_prj ID"
   214 
   215 lemma cast_u_liftdefl:
   216   "cast\<cdot>(u_liftdefl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
   217 unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u)
   218 
   219 lemma u_liftdefl_liftdefl_of:
   220   "u_liftdefl\<cdot>(liftdefl_of\<cdot>A) = u_defl\<cdot>A"
   221 by (rule cast_eq_imp_eq)
   222    (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
   223 
   224 subsection \<open>Class instance proofs\<close>
   225 
   226 subsubsection \<open>Universal domain\<close>
   227 
   228 instantiation udom :: "domain"
   229 begin
   230 
   231 definition [simp]:
   232   "emb = (ID :: udom \<rightarrow> udom)"
   233 
   234 definition [simp]:
   235   "prj = (ID :: udom \<rightarrow> udom)"
   236 
   237 definition
   238   "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
   239 
   240 definition
   241   "(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb"
   242 
   243 definition
   244   "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
   245 
   246 definition
   247   "liftdefl (t::udom itself) = liftdefl_of\<cdot>DEFL(udom)"
   248 
   249 instance 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
   264 qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+
   265 
   266 end
   267 
   268 subsubsection \<open>Lifted cpo\<close>
   269 
   270 instantiation u :: (predomain) "domain"
   271 begin
   272 
   273 definition
   274   "emb = u_emb oo liftemb"
   275 
   276 definition
   277   "prj = liftprj oo u_prj"
   278 
   279 definition
   280   "defl (t::'a u itself) = u_liftdefl\<cdot>LIFTDEFL('a)"
   281 
   282 definition
   283   "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
   284 
   285 definition
   286   "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
   287 
   288 definition
   289   "liftdefl (t::'a u itself) = liftdefl_of\<cdot>DEFL('a u)"
   290 
   291 instance 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)
   298 qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
   299 
   300 end
   301 
   302 lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)"
   303 by (rule defl_u_def)
   304 
   305 subsubsection \<open>Strict function space\<close>
   306 
   307 instantiation sfun :: ("domain", "domain") "domain"
   308 begin
   309 
   310 definition
   311   "emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb"
   312 
   313 definition
   314   "prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj"
   315 
   316 definition
   317   "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   318 
   319 definition
   320   "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
   321 
   322 definition
   323   "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
   324 
   325 definition
   326   "liftdefl (t::('a \<rightarrow>! 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow>! 'b)"
   327 
   328 instance 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)
   335 qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+
   336 
   337 end
   338 
   339 lemma DEFL_sfun:
   340   "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   341 by (rule defl_sfun_def)
   342 
   343 subsubsection \<open>Continuous function space\<close>
   344 
   345 instantiation cfun :: (predomain, "domain") "domain"
   346 begin
   347 
   348 definition
   349   "emb = emb oo encode_cfun"
   350 
   351 definition
   352   "prj = decode_cfun oo prj"
   353 
   354 definition
   355   "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
   356 
   357 definition
   358   "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
   359 
   360 definition
   361   "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
   362 
   363 definition
   364   "liftdefl (t::('a \<rightarrow> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow> 'b)"
   365 
   366 instance 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)
   375 qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+
   376 
   377 end
   378 
   379 lemma DEFL_cfun:
   380   "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
   381 by (rule defl_cfun_def)
   382 
   383 subsubsection \<open>Strict product\<close>
   384 
   385 instantiation sprod :: ("domain", "domain") "domain"
   386 begin
   387 
   388 definition
   389   "emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb"
   390 
   391 definition
   392   "prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj"
   393 
   394 definition
   395   "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   396 
   397 definition
   398   "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
   399 
   400 definition
   401   "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
   402 
   403 definition
   404   "liftdefl (t::('a \<otimes> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<otimes> 'b)"
   405 
   406 instance 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)
   413 qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+
   414 
   415 end
   416 
   417 lemma DEFL_sprod:
   418   "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   419 by (rule defl_sprod_def)
   420 
   421 subsubsection \<open>Cartesian product\<close>
   422 
   423 definition 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 
   427 lemma 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)"
   431 unfolding prod_liftdefl_def
   432 apply (rule cast_defl_fun2)
   433 apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod)
   434 apply (simp add: ep_pair.intro)
   435 apply (erule (1) finite_deflation_sprod_map)
   436 done
   437 
   438 instantiation prod :: (predomain, predomain) predomain
   439 begin
   440 
   441 definition
   442   "liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo
   443     (sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)"
   444 
   445 definition
   446   "liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo
   447     (encode_prod_u oo u_map\<cdot>prod_prj)"
   448 
   449 definition
   450   "liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
   451 
   452 instance 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)
   460 qed
   461 
   462 end
   463 
   464 instantiation prod :: ("domain", "domain") "domain"
   465 begin
   466 
   467 definition
   468   "emb = prod_emb oo prod_map\<cdot>emb\<cdot>emb"
   469 
   470 definition
   471   "prj = prod_map\<cdot>prj\<cdot>prj oo prod_prj"
   472 
   473 definition
   474   "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   475 
   476 instance 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)
   496 qed
   497 
   498 end
   499 
   500 lemma DEFL_prod:
   501   "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   502 by (rule defl_prod_def)
   503 
   504 lemma LIFTDEFL_prod:
   505   "LIFTDEFL('a::predomain \<times> 'b::predomain) =
   506     prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
   507 by (rule liftdefl_prod_def)
   508 
   509 subsubsection \<open>Unit type\<close>
   510 
   511 instantiation unit :: "domain"
   512 begin
   513 
   514 definition
   515   "emb = (\<bottom> :: unit \<rightarrow> udom)"
   516 
   517 definition
   518   "prj = (\<bottom> :: udom \<rightarrow> unit)"
   519 
   520 definition
   521   "defl (t::unit itself) = \<bottom>"
   522 
   523 definition
   524   "(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb"
   525 
   526 definition
   527   "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
   528 
   529 definition
   530   "liftdefl (t::unit itself) = liftdefl_of\<cdot>DEFL(unit)"
   531 
   532 instance 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
   538 qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+
   539 
   540 end
   541 
   542 subsubsection \<open>Discrete cpo\<close>
   543 
   544 instantiation discr :: (countable) predomain
   545 begin
   546 
   547 definition
   548   "(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx"
   549 
   550 definition
   551   "(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID"
   552 
   553 definition
   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 
   557 instance 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
   583 qed
   584 
   585 end
   586 
   587 subsubsection \<open>Strict sum\<close>
   588 
   589 instantiation ssum :: ("domain", "domain") "domain"
   590 begin
   591 
   592 definition
   593   "emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb"
   594 
   595 definition
   596   "prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj"
   597 
   598 definition
   599   "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   600 
   601 definition
   602   "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
   603 
   604 definition
   605   "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
   606 
   607 definition
   608   "liftdefl (t::('a \<oplus> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<oplus> 'b)"
   609 
   610 instance 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)
   617 qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+
   618 
   619 end
   620 
   621 lemma DEFL_ssum:
   622   "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   623 by (rule defl_ssum_def)
   624 
   625 subsubsection \<open>Lifted HOL type\<close>
   626 
   627 instantiation lift :: (countable) "domain"
   628 begin
   629 
   630 definition
   631   "emb = emb oo (\<Lambda> x. Rep_lift x)"
   632 
   633 definition
   634   "prj = (\<Lambda> y. Abs_lift y) oo prj"
   635 
   636 definition
   637   "defl (t::'a lift itself) = DEFL('a discr u)"
   638 
   639 definition
   640   "(liftemb :: 'a lift u \<rightarrow> udom u) = u_map\<cdot>emb"
   641 
   642 definition
   643   "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
   644 
   645 definition
   646   "liftdefl (t::'a lift itself) = liftdefl_of\<cdot>DEFL('a lift)"
   647 
   648 instance 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)
   658 qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+
   659 
   660 end
   661 
   662 end