src/HOL/HOLCF/ConvexPD.thy

     done
   thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Convex powerdomain is a domain *}
+subsection {* Convex powerdomain is bifinite *}
 
 lemma approx_chain_convex_map:
   assumes "approx_chain a"
   shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))"
   using assms unfolding approx_chain_def

 proof
   show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
     using bifinite [where 'a='a]
     by (fast intro!: approx_chain_convex_map)
 qed
-
-definition
-  convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
-where
-  "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
-
-lemma convex_approx: "approx_chain convex_approx"
-using convex_map_ID finite_deflation_convex_map
-unfolding convex_approx_def by (rule approx_chain_lemma1)
-
-definition convex_defl :: "udom defl \<rightarrow> udom defl"
-where "convex_defl = defl_fun1 convex_approx convex_map"
-
-lemma cast_convex_defl:
-  "cast\<cdot>(convex_defl\<cdot>A) =
-    udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
-using convex_approx finite_deflation_convex_map
-unfolding convex_defl_def by (rule cast_defl_fun1)
-
-instantiation convex_pd :: ("domain") liftdomain
-begin
-
-definition
-  "emb = udom_emb convex_approx oo convex_map\<cdot>emb"
-
-definition
-  "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
-
-definition
-  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
-
-definition
-  "(liftemb :: 'a convex_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
-  "(liftprj :: udom \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
-  "liftdefl (t::'a convex_pd itself) = u_defl\<cdot>DEFL('a convex_pd)"
-
-instance
-using liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def
-proof (rule liftdomain_class_intro)
-  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
-    unfolding emb_convex_pd_def prj_convex_pd_def
-    using ep_pair_udom [OF convex_approx]
-    by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
-next
-  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
-    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
-    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
-qed
-
-end
-
-text {* DEFL of type constructor = type combinator *}
-
-lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
-by (rule defl_convex_pd_def)
-
 
 subsection {* Join *}
 
 definition
   convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where