src/HOLCF/ConvexPD.thy

 
 typedef (open) 'a convex_pd =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (fast intro: convex_le.ideal_principal)
 
-instantiation convex_pd :: (bifinite) below
+instantiation convex_pd :: ("domain") below
 begin
 
 definition
   "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y"
 
 instance ..
 end
 
-instance convex_pd :: (bifinite) po
+instance convex_pd :: ("domain") po
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_po)
 
-instance convex_pd :: (bifinite) cpo
+instance convex_pd :: ("domain") cpo
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_cpo)
 
 definition
   convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where

 text {* Convex powerdomain is pointed *}
 
 lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: convex_pd.principal_induct, simp, simp)
 
-instance convex_pd :: (bifinite) pcpo
+instance convex_pd :: ("domain") pcpo
 by intro_classes (fast intro: convex_pd_minimal)
 
 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
 by (rule convex_pd_minimal [THEN UU_I, symmetric])
 

     done
   thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Convex powerdomain is a bifinite domain *}
+subsection {* Convex powerdomain is a domain *}
 
 definition
   convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
 where
   "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"

   "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 :: (bifinite) liftdomain
+instantiation convex_pd :: ("domain") liftdomain
 begin
 
 definition
   "emb = udom_emb convex_approx oo convex_map\<cdot>emb"