src/HOLCF/Library/Defl_Bifinite.thy
changeset 40491 6de5839e2fb3
parent 40002 c5b5f7a3a3b1
child 40494 db8a09daba7b
     1.1 --- a/src/HOLCF/Library/Defl_Bifinite.thy	Tue Nov 09 08:41:36 2010 -0800
     1.2 +++ b/src/HOLCF/Library/Defl_Bifinite.thy	Tue Nov 09 16:37:13 2010 -0800
     1.3 @@ -622,7 +622,18 @@
     1.4    "defl (t::defl itself) =
     1.5      (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
     1.6  
     1.7 -instance proof
     1.8 +definition
     1.9 +  "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    1.10 +
    1.11 +definition
    1.12 +  "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
    1.13 +
    1.14 +definition
    1.15 +  "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
    1.16 +
    1.17 +instance
    1.18 +using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
    1.19 +proof (rule bifinite_class_intro)
    1.20    show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
    1.21      unfolding emb_defl_def prj_defl_def
    1.22      by (rule ep_pair_udom [OF defl_approx])