src/HOL/HOLCF/Representable.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63040 eb4ddd18d635 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
tuned proofs;
```     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 "~~/src/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
```