# Theory Representable

Up to index of Isabelle/HOL/HOLCF

theory Representable
imports Algebraic
`(*  Title:      HOL/HOLCF/Representable.thy    Author:     Brian Huffman*)header {* Representable domains *}theory Representableimports Algebraic Map_Functions "~~/src/HOL/Library/Countable"begindefault_sort cposubsection {* Class of representable domains *}text {*  We define a ``domain'' as a pcpo that is isomorphic to some  algebraic deflation over the universal domain; this is equivalent  to being omega-bifinite.  A predomain is a cpo that, when lifted, becomes a domain.  Predomains are represented by deflations over a lifted universal  domain type.*}class predomain_syn = cpo +  fixes liftemb :: "'a⇩⊥ -> udom⇩⊥"  fixes liftprj :: "udom⇩⊥ -> 'a⇩⊥"  fixes liftdefl :: "'a itself => udom u defl"class predomain = predomain_syn +  assumes predomain_ep: "ep_pair liftemb liftprj"  assumes cast_liftdefl: "cast·(liftdefl TYPE('a)) = liftemb oo liftprj"syntax "_LIFTDEFL" :: "type => logic"  ("(1LIFTDEFL/(1'(_')))")translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"definition liftdefl_of :: "udom defl -> udom u defl"  where "liftdefl_of = defl_fun1 ID ID u_map"lemma cast_liftdefl_of: "cast·(liftdefl_of·t) = u_map·(cast·t)"by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)class "domain" = predomain_syn + pcpo +  fixes emb :: "'a -> udom"  fixes prj :: "udom -> 'a"  fixes defl :: "'a itself => udom defl"  assumes ep_pair_emb_prj: "ep_pair emb prj"  assumes cast_DEFL: "cast·(defl TYPE('a)) = emb oo prj"  assumes liftemb_eq: "liftemb = u_map·emb"  assumes liftprj_eq: "liftprj = u_map·prj"  assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of·(defl TYPE('a))"syntax "_DEFL" :: "type => logic"  ("(1DEFL/(1'(_')))")translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"instance "domain" ⊆ predomainproof  show "ep_pair liftemb (liftprj::udom⇩⊥ -> 'a⇩⊥)"    unfolding liftemb_eq liftprj_eq    by (intro ep_pair_u_map ep_pair_emb_prj)  show "cast·LIFTDEFL('a) = liftemb oo (liftprj::udom⇩⊥ -> 'a⇩⊥)"    unfolding liftemb_eq liftprj_eq liftdefl_eq    by (simp add: cast_liftdefl_of cast_DEFL u_map_oo)qedtext {*  Constants @{const liftemb} and @{const liftprj} imply class predomain.*}setup {*  fold Sign.add_const_constraint  [(@{const_name liftemb}, SOME @{typ "'a::predomain u -> udom u"}),   (@{const_name liftprj}, SOME @{typ "udom u -> 'a::predomain u"}),   (@{const_name liftdefl}, SOME @{typ "'a::predomain itself => udom u defl"})]*}interpretation predomain: pcpo_ep_pair liftemb liftprj  unfolding pcpo_ep_pair_def by (rule predomain_ep)interpretation "domain": pcpo_ep_pair emb prj  unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj)lemmas emb_inverse = domain.e_inverselemmas emb_prj_below = domain.e_p_belowlemmas emb_eq_iff = domain.e_eq_ifflemmas emb_strict = domain.e_strictlemmas prj_strict = domain.p_strictsubsection {* Domains are bifinite *}lemma approx_chain_ep_cast:  assumes ep: "ep_pair (e::'a::pcpo -> 'b::bifinite) (p::'b -> 'a)"  assumes cast_t: "cast·t = e oo p"  shows "∃(a::nat => 'a::pcpo -> 'a). approx_chain a"proof -  interpret ep_pair e p by fact  obtain Y where Y: "∀i. Y i \<sqsubseteq> Y (Suc i)"  and t: "t = (\<Squnion>i. defl_principal (Y i))"    by (rule defl.obtain_principal_chain)  def approx ≡ "λi. (p oo cast·(defl_principal (Y i)) oo e) :: 'a -> 'a"  have "approx_chain approx"  proof (rule approx_chain.intro)    show "chain (λi. approx i)"      unfolding approx_def by (simp add: Y)    show "(\<Squnion>i. approx i) = ID"      unfolding approx_def      by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)    show "!!i. finite_deflation (approx i)"      unfolding approx_def      apply (rule finite_deflation_p_d_e)      apply (rule finite_deflation_cast)      apply (rule defl.compact_principal)      apply (rule below_trans [OF monofun_cfun_fun])      apply (rule is_ub_thelub, simp add: Y)      apply (simp add: lub_distribs Y t [symmetric] cast_t)      done  qed  thus "∃(a::nat => 'a -> 'a). approx_chain a" by - (rule exI)qedinstance "domain" ⊆ bifiniteby default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])instance predomain ⊆ profiniteby default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])subsection {* Universal domain ep-pairs *}definition "u_emb = udom_emb (λi. u_map·(udom_approx i))"definition "u_prj = udom_prj (λi. u_map·(udom_approx i))"definition "prod_emb = udom_emb (λi. prod_map·(udom_approx i)·(udom_approx i))"definition "prod_prj = udom_prj (λi. prod_map·(udom_approx i)·(udom_approx i))"definition "sprod_emb = udom_emb (λi. sprod_map·(udom_approx i)·(udom_approx i))"definition "sprod_prj = udom_prj (λi. sprod_map·(udom_approx i)·(udom_approx i))"definition "ssum_emb = udom_emb (λi. ssum_map·(udom_approx i)·(udom_approx i))"definition "ssum_prj = udom_prj (λi. ssum_map·(udom_approx i)·(udom_approx i))"definition "sfun_emb = udom_emb (λi. sfun_map·(udom_approx i)·(udom_approx i))"definition "sfun_prj = udom_prj (λi. sfun_map·(udom_approx i)·(udom_approx i))"lemma ep_pair_u: "ep_pair u_emb u_prj"  unfolding u_emb_def u_prj_def  by (simp add: ep_pair_udom approx_chain_u_map)lemma ep_pair_prod: "ep_pair prod_emb prod_prj"  unfolding prod_emb_def prod_prj_def  by (simp add: ep_pair_udom approx_chain_prod_map)lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"  unfolding sprod_emb_def sprod_prj_def  by (simp add: ep_pair_udom approx_chain_sprod_map)lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj"  unfolding ssum_emb_def ssum_prj_def  by (simp add: ep_pair_udom approx_chain_ssum_map)lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj"  unfolding sfun_emb_def sfun_prj_def  by (simp add: ep_pair_udom approx_chain_sfun_map)subsection {* Type combinators *}definition u_defl :: "udom defl -> udom defl"  where "u_defl = defl_fun1 u_emb u_prj u_map"definition prod_defl :: "udom defl -> udom defl -> udom defl"  where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"definition sprod_defl :: "udom defl -> udom defl -> udom defl"  where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"definition ssum_defl :: "udom defl -> udom defl -> udom defl"where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"definition sfun_defl :: "udom defl -> udom defl -> udom defl"  where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"lemma cast_u_defl:  "cast·(u_defl·A) = u_emb oo u_map·(cast·A) oo u_prj"using ep_pair_u finite_deflation_u_mapunfolding u_defl_def by (rule cast_defl_fun1)lemma cast_prod_defl:  "cast·(prod_defl·A·B) =    prod_emb oo prod_map·(cast·A)·(cast·B) oo prod_prj"using ep_pair_prod finite_deflation_prod_mapunfolding prod_defl_def by (rule cast_defl_fun2)lemma cast_sprod_defl:  "cast·(sprod_defl·A·B) =    sprod_emb oo sprod_map·(cast·A)·(cast·B) oo sprod_prj"using ep_pair_sprod finite_deflation_sprod_mapunfolding sprod_defl_def by (rule cast_defl_fun2)lemma cast_ssum_defl:  "cast·(ssum_defl·A·B) =    ssum_emb oo ssum_map·(cast·A)·(cast·B) oo ssum_prj"using ep_pair_ssum finite_deflation_ssum_mapunfolding ssum_defl_def by (rule cast_defl_fun2)lemma cast_sfun_defl:  "cast·(sfun_defl·A·B) =    sfun_emb oo sfun_map·(cast·A)·(cast·B) oo sfun_prj"using ep_pair_sfun finite_deflation_sfun_mapunfolding sfun_defl_def by (rule cast_defl_fun2)text {* Special deflation combinator for unpointed types. *}definition u_liftdefl :: "udom u defl -> udom defl"  where "u_liftdefl = defl_fun1 u_emb u_prj ID"lemma cast_u_liftdefl:  "cast·(u_liftdefl·A) = u_emb oo cast·A oo u_prj"unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u)lemma u_liftdefl_liftdefl_of:  "u_liftdefl·(liftdefl_of·A) = u_defl·A"by (rule cast_eq_imp_eq)   (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)subsection {* Class instance proofs *}subsubsection {* Universal domain *}instantiation udom :: "domain"begindefinition [simp]:  "emb = (ID :: udom -> udom)"definition [simp]:  "prj = (ID :: udom -> udom)"definition  "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"definition  "(liftemb :: udom u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> udom u) = u_map·prj"definition  "liftdefl (t::udom itself) = liftdefl_of·DEFL(udom)"instance proof  show "ep_pair emb (prj :: udom -> udom)"    by (simp add: ep_pair.intro)  show "cast·DEFL(udom) = emb oo (prj :: udom -> udom)"    unfolding defl_udom_def    apply (subst contlub_cfun_arg)    apply (rule chainI)    apply (rule defl.principal_mono)    apply (simp add: below_fin_defl_def)    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)    apply (rule chainE)    apply (rule chain_udom_approx)    apply (subst cast_defl_principal)    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)    doneqed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+endsubsubsection {* Lifted cpo *}instantiation u :: (predomain) "domain"begindefinition  "emb = u_emb oo liftemb"definition  "prj = liftprj oo u_prj"definition  "defl (t::'a u itself) = u_liftdefl·LIFTDEFL('a)"definition  "(liftemb :: 'a u u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> 'a u u) = u_map·prj"definition  "liftdefl (t::'a u itself) = liftdefl_of·DEFL('a u)"instance proof  show "ep_pair emb (prj :: udom -> 'a u)"    unfolding emb_u_def prj_u_def    by (intro ep_pair_comp ep_pair_u predomain_ep)  show "cast·DEFL('a u) = emb oo (prj :: udom -> 'a u)"    unfolding emb_u_def prj_u_def defl_u_def    by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo)qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+endlemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl·LIFTDEFL('a)"by (rule defl_u_def)subsubsection {* Strict function space *}instantiation sfun :: ("domain", "domain") "domain"begindefinition  "emb = sfun_emb oo sfun_map·prj·emb"definition  "prj = sfun_map·emb·prj oo sfun_prj"definition  "defl (t::('a ->! 'b) itself) = sfun_defl·DEFL('a)·DEFL('b)"definition  "(liftemb :: ('a ->! 'b) u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> ('a ->! 'b) u) = u_map·prj"definition  "liftdefl (t::('a ->! 'b) itself) = liftdefl_of·DEFL('a ->! 'b)"instance proof  show "ep_pair emb (prj :: udom -> 'a ->! 'b)"    unfolding emb_sfun_def prj_sfun_def    by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)  show "cast·DEFL('a ->! 'b) = emb oo (prj :: udom -> 'a ->! 'b)"    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl    by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+endlemma DEFL_sfun:  "DEFL('a::domain ->! 'b::domain) = sfun_defl·DEFL('a)·DEFL('b)"by (rule defl_sfun_def)subsubsection {* Continuous function space *}instantiation cfun :: (predomain, "domain") "domain"begindefinition  "emb = emb oo encode_cfun"definition  "prj = decode_cfun oo prj"definition  "defl (t::('a -> 'b) itself) = DEFL('a u ->! 'b)"definition  "(liftemb :: ('a -> 'b) u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> ('a -> 'b) u) = u_map·prj"definition  "liftdefl (t::('a -> 'b) itself) = liftdefl_of·DEFL('a -> 'b)"instance proof  have "ep_pair encode_cfun decode_cfun"    by (rule ep_pair.intro, simp_all)  thus "ep_pair emb (prj :: udom -> 'a -> 'b)"    unfolding emb_cfun_def prj_cfun_def    using ep_pair_emb_prj by (rule ep_pair_comp)  show "cast·DEFL('a -> 'b) = emb oo (prj :: udom -> 'a -> 'b)"    unfolding emb_cfun_def prj_cfun_def defl_cfun_def    by (simp add: cast_DEFL cfcomp1)qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+endlemma DEFL_cfun:  "DEFL('a::predomain -> 'b::domain) = DEFL('a u ->! 'b)"by (rule defl_cfun_def)subsubsection {* Strict product *}instantiation sprod :: ("domain", "domain") "domain"begindefinition  "emb = sprod_emb oo sprod_map·emb·emb"definition  "prj = sprod_map·prj·prj oo sprod_prj"definition  "defl (t::('a ⊗ 'b) itself) = sprod_defl·DEFL('a)·DEFL('b)"definition  "(liftemb :: ('a ⊗ 'b) u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> ('a ⊗ 'b) u) = u_map·prj"definition  "liftdefl (t::('a ⊗ 'b) itself) = liftdefl_of·DEFL('a ⊗ 'b)"instance proof  show "ep_pair emb (prj :: udom -> 'a ⊗ 'b)"    unfolding emb_sprod_def prj_sprod_def    by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)  show "cast·DEFL('a ⊗ 'b) = emb oo (prj :: udom -> 'a ⊗ 'b)"    unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl    by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+endlemma DEFL_sprod:  "DEFL('a::domain ⊗ 'b::domain) = sprod_defl·DEFL('a)·DEFL('b)"by (rule defl_sprod_def)subsubsection {* Cartesian product *}definition prod_liftdefl :: "udom u defl -> udom u defl -> udom u defl"  where "prod_liftdefl = defl_fun2 (u_map·prod_emb oo decode_prod_u)    (encode_prod_u oo u_map·prod_prj) sprod_map"lemma cast_prod_liftdefl:  "cast·(prod_liftdefl·a·b) =    (u_map·prod_emb oo decode_prod_u) oo sprod_map·(cast·a)·(cast·b) oo      (encode_prod_u oo u_map·prod_prj)"unfolding prod_liftdefl_defapply (rule cast_defl_fun2)apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod)apply (simp add: ep_pair.intro)apply (erule (1) finite_deflation_sprod_map)doneinstantiation prod :: (predomain, predomain) predomainbegindefinition  "liftemb = (u_map·prod_emb oo decode_prod_u) oo    (sprod_map·liftemb·liftemb oo encode_prod_u)"definition  "liftprj = (decode_prod_u oo sprod_map·liftprj·liftprj) oo    (encode_prod_u oo u_map·prod_prj)"definition  "liftdefl (t::('a × 'b) itself) = prod_liftdefl·LIFTDEFL('a)·LIFTDEFL('b)"instance proof  show "ep_pair liftemb (liftprj :: udom u -> ('a × 'b) u)"    unfolding liftemb_prod_def liftprj_prod_def    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map       ep_pair_prod predomain_ep, simp_all add: ep_pair.intro)  show "cast·LIFTDEFL('a × 'b) = liftemb oo (liftprj :: udom u -> ('a × 'b) u)"    unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def    by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map)qedendinstantiation prod :: ("domain", "domain") "domain"begindefinition  "emb = prod_emb oo prod_map·emb·emb"definition  "prj = prod_map·prj·prj oo prod_prj"definition  "defl (t::('a × 'b) itself) = prod_defl·DEFL('a)·DEFL('b)"instance proof  show 1: "ep_pair emb (prj :: udom -> 'a × 'b)"    unfolding emb_prod_def prj_prod_def    by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj)  show 2: "cast·DEFL('a × 'b) = emb oo (prj :: udom -> 'a × 'b)"    unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl    by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map)  show 3: "liftemb = u_map·(emb :: 'a × 'b -> udom)"    unfolding emb_prod_def liftemb_prod_def liftemb_eq    unfolding encode_prod_u_def decode_prod_u_def    by (rule cfun_eqI, case_tac x, simp, clarsimp)  show 4: "liftprj = u_map·(prj :: udom -> 'a × 'b)"    unfolding prj_prod_def liftprj_prod_def liftprj_eq    unfolding encode_prod_u_def decode_prod_u_def    apply (rule cfun_eqI, case_tac x, simp)    apply (rename_tac y, case_tac "prod_prj·y", simp)    done  show 5: "LIFTDEFL('a × 'b) = liftdefl_of·DEFL('a × 'b)"    by (rule cast_eq_imp_eq)      (simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo)qedendlemma DEFL_prod:  "DEFL('a::domain × 'b::domain) = prod_defl·DEFL('a)·DEFL('b)"by (rule defl_prod_def)lemma LIFTDEFL_prod:  "LIFTDEFL('a::predomain × 'b::predomain) =    prod_liftdefl·LIFTDEFL('a)·LIFTDEFL('b)"by (rule liftdefl_prod_def)subsubsection {* Unit type *}instantiation unit :: "domain"begindefinition  "emb = (⊥ :: unit -> udom)"definition  "prj = (⊥ :: udom -> unit)"definition  "defl (t::unit itself) = ⊥"definition  "(liftemb :: unit u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> unit u) = u_map·prj"definition  "liftdefl (t::unit itself) = liftdefl_of·DEFL(unit)"instance proof  show "ep_pair emb (prj :: udom -> unit)"    unfolding emb_unit_def prj_unit_def    by (simp add: ep_pair.intro)  show "cast·DEFL(unit) = emb oo (prj :: udom -> unit)"    unfolding emb_unit_def prj_unit_def defl_unit_def by simpqed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+endsubsubsection {* Discrete cpo *}instantiation discr :: (countable) predomainbegindefinition  "(liftemb :: 'a discr u -> udom u) = strictify·up oo udom_emb discr_approx"definition  "(liftprj :: udom u -> 'a discr u) = udom_prj discr_approx oo fup·ID"definition  "liftdefl (t::'a discr itself) =    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u -> 'a discr u))))"instance proof  show 1: "ep_pair liftemb (liftprj :: udom u -> 'a discr u)"    unfolding liftemb_discr_def liftprj_discr_def    apply (intro ep_pair_comp ep_pair_udom [OF discr_approx])    apply (rule ep_pair.intro)    apply (simp add: strictify_conv_if)    apply (case_tac y, simp, simp add: strictify_conv_if)    done  show "cast·LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u -> 'a discr u)"    unfolding liftdefl_discr_def    apply (subst contlub_cfun_arg)    apply (rule chainI)    apply (rule defl.principal_mono)    apply (simp add: below_fin_defl_def)    apply (simp add: Abs_fin_defl_inverse        ep_pair.finite_deflation_e_d_p [OF 1]        approx_chain.finite_deflation_approx [OF discr_approx])    apply (intro monofun_cfun below_refl)    apply (rule chainE)    apply (rule chain_discr_approx)    apply (subst cast_defl_principal)    apply (simp add: Abs_fin_defl_inverse        ep_pair.finite_deflation_e_d_p [OF 1]        approx_chain.finite_deflation_approx [OF discr_approx])    apply (simp add: lub_distribs)    doneqedendsubsubsection {* Strict sum *}instantiation ssum :: ("domain", "domain") "domain"begindefinition  "emb = ssum_emb oo ssum_map·emb·emb"definition  "prj = ssum_map·prj·prj oo ssum_prj"definition  "defl (t::('a ⊕ 'b) itself) = ssum_defl·DEFL('a)·DEFL('b)"definition  "(liftemb :: ('a ⊕ 'b) u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> ('a ⊕ 'b) u) = u_map·prj"definition  "liftdefl (t::('a ⊕ 'b) itself) = liftdefl_of·DEFL('a ⊕ 'b)"instance proof  show "ep_pair emb (prj :: udom -> 'a ⊕ 'b)"    unfolding emb_ssum_def prj_ssum_def    by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)  show "cast·DEFL('a ⊕ 'b) = emb oo (prj :: udom -> 'a ⊕ 'b)"    unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl    by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+endlemma DEFL_ssum:  "DEFL('a::domain ⊕ 'b::domain) = ssum_defl·DEFL('a)·DEFL('b)"by (rule defl_ssum_def)subsubsection {* Lifted HOL type *}instantiation lift :: (countable) "domain"begindefinition  "emb = emb oo (Λ x. Rep_lift x)"definition  "prj = (Λ y. Abs_lift y) oo prj"definition  "defl (t::'a lift itself) = DEFL('a discr u)"definition  "(liftemb :: 'a lift u -> udom u) = u_map·emb"definition  "(liftprj :: udom u -> 'a lift u) = u_map·prj"definition  "liftdefl (t::'a lift itself) = liftdefl_of·DEFL('a lift)"instance proof  note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse  have "ep_pair (Λ(x::'a lift). Rep_lift x) (Λ y. Abs_lift y)"    by (simp add: ep_pair_def)  thus "ep_pair emb (prj :: udom -> 'a lift)"    unfolding emb_lift_def prj_lift_def    using ep_pair_emb_prj by (rule ep_pair_comp)  show "cast·DEFL('a lift) = emb oo (prj :: udom -> 'a lift)"    unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL    by (simp add: cfcomp1)qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+endend`