# HG changeset patch
# User huffman
# Date 1286548790 25200
# Node ID 38677db30cadd293ef208453f7d20dc9ca450d2d
# Parent  310f9858510780f754b6ca381d717b157338d7a4
rename class 'sfp' to 'bifinite'

diff -r 310f98585107 -r 38677db30cad src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Bifinite.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -8,14 +8,14 @@
 imports Algebraic
 begin
 
-subsection {* Class of SFP domains *}
+subsection {* Class of bifinite domains *}
 
 text {*
-  We define a SFP domain as a pcpo that is isomorphic to some
+  We define a bifinite domain as a pcpo that is isomorphic to some
   algebraic deflation over the universal domain.
 *}
 
-class sfp = pcpo +
+class bifinite = pcpo +
   fixes emb :: "'a::pcpo \<rightarrow> udom"
   fixes prj :: "udom \<rightarrow> 'a::pcpo"
   fixes sfp :: "'a itself \<Rightarrow> sfp"
@@ -25,26 +25,26 @@
 syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
 translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
 
-interpretation sfp:
-  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
+interpretation bifinite:
+  pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
   unfolding pcpo_ep_pair_def
   by (rule ep_pair_emb_prj)
 
-lemmas emb_inverse = sfp.e_inverse
-lemmas emb_prj_below = sfp.e_p_below
-lemmas emb_eq_iff = sfp.e_eq_iff
-lemmas emb_strict = sfp.e_strict
-lemmas prj_strict = sfp.p_strict
+lemmas emb_inverse = bifinite.e_inverse
+lemmas emb_prj_below = bifinite.e_p_below
+lemmas emb_eq_iff = bifinite.e_eq_iff
+lemmas emb_strict = bifinite.e_strict
+lemmas prj_strict = bifinite.p_strict
 
-subsection {* SFP domains have a countable compact basis *}
+subsection {* Bifinite domains have a countable compact basis *}
 
 text {*
   Eventually it should be possible to generalize this to an unpointed
-  variant of the sfp class.
+  variant of the bifinite class.
 *}
 
 interpretation compact_basis:
-  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
+  ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
 proof -
   obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
   and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
@@ -59,7 +59,7 @@
       by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
     show "\<And>i. finite_deflation (approx i)"
       unfolding approx_def
-      apply (rule sfp.finite_deflation_p_d_e)
+      apply (rule bifinite.finite_deflation_p_d_e)
       apply (rule finite_deflation_cast)
       apply (rule sfp.compact_principal)
       apply (rule below_trans [OF monofun_cfun_fun])
@@ -146,7 +146,7 @@
 
 subsection {* Instance for universal domain type *}
 
-instantiation udom :: sfp
+instantiation udom :: bifinite
 begin
 
 definition [simp]:
@@ -208,7 +208,7 @@
 apply (erule (1) finite_deflation_cfun_map)
 done
 
-instantiation cfun :: (sfp, sfp) sfp
+instantiation cfun :: (bifinite, bifinite) bifinite
 begin
 
 definition
@@ -233,7 +233,8 @@
 
 end
 
-lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_cfun:
+  "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
 by (rule sfp_cfun_def)
 
 end
diff -r 310f98585107 -r 38677db30cad src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -8,7 +8,7 @@
 imports Bifinite
 begin
 
-default_sort sfp
+default_sort bifinite
 
 subsection {* A compact basis for powerdomains *}
 
@@ -24,7 +24,7 @@
 
 text {* The powerdomain basis type is countable. *}
 
-lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f"
+lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
 proof -
   obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
     using compact_basis.countable ..
diff -r 310f98585107 -r 38677db30cad src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -123,7 +123,7 @@
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (fast intro: convex_le.ideal_principal)
 
-instantiation convex_pd :: (sfp) below
+instantiation convex_pd :: (bifinite) below
 begin
 
 definition
@@ -132,11 +132,11 @@
 instance ..
 end
 
-instance convex_pd :: (sfp) po
+instance convex_pd :: (bifinite) po
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_po)
 
-instance convex_pd :: (sfp) cpo
+instance convex_pd :: (bifinite) cpo
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_cpo)
 
@@ -155,7 +155,7 @@
 lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: convex_pd.principal_induct, simp, simp)
 
-instance convex_pd :: (sfp) pcpo
+instance convex_pd :: (bifinite) pcpo
 by intro_classes (fast intro: convex_pd_minimal)
 
 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
@@ -444,7 +444,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Convex powerdomain is an SFP domain *}
+subsection {* Convex powerdomain is a bifinite domain *}
 
 definition
   convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
@@ -474,7 +474,7 @@
 apply (erule finite_deflation_convex_map)
 done
 
-instantiation convex_pd :: (sfp) sfp
+instantiation convex_pd :: (bifinite) bifinite
 begin
 
 definition
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Cprod.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -97,7 +97,7 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
-subsection {* Cartesian product is an SFP domain *}
+subsection {* Cartesian product is a bifinite domain *}
 
 definition
   prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
@@ -127,7 +127,7 @@
 apply (erule (1) finite_deflation_cprod_map)
 done
 
-instantiation prod :: (sfp, sfp) sfp
+instantiation prod :: (bifinite, bifinite) bifinite
 begin
 
 definition
@@ -152,7 +152,8 @@
 
 end
 
-lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_prod:
+  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
 by (rule sfp_prod_def)
 
 end
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Library/Strict_Fun.thy
--- a/src/HOLCF/Library/Strict_Fun.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -143,7 +143,7 @@
          deflation_strict `deflation d1` `deflation d2`)
 qed
 
-subsection {* Strict function space is an SFP domain *}
+subsection {* Strict function space is a bifinite domain *}
 
 definition
   sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
@@ -173,7 +173,7 @@
 apply (erule (1) finite_deflation_sfun_map)
 done
 
-instantiation sfun :: (sfp, sfp) sfp
+instantiation sfun :: (bifinite, bifinite) bifinite
 begin
 
 definition
@@ -198,9 +198,8 @@
 
 end
 
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sfun: "SFP('a::sfp \<rightarrow>! 'b::sfp) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_sfun:
+  "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
 by (rule sfp_sfun_def)
 
 lemma isodefl_sfun:
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Lift.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -171,7 +171,7 @@
 by (cases x, simp_all)
 
 
-subsection {* Lifted countable types are SFP domains *}
+subsection {* Lifted countable types are bifinite domains *}
 
 definition
   lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
@@ -220,7 +220,7 @@
 using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
 by (rule approx_chain.intro)
 
-instantiation lift :: (countable) sfp
+instantiation lift :: (countable) bifinite
 begin
 
 definition
diff -r 310f98585107 -r 38677db30cad src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -78,7 +78,7 @@
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (fast intro: lower_le.ideal_principal)
 
-instantiation lower_pd :: (sfp) below
+instantiation lower_pd :: (bifinite) below
 begin
 
 definition
@@ -87,11 +87,11 @@
 instance ..
 end
 
-instance lower_pd :: (sfp) po
+instance lower_pd :: (bifinite) po
 using type_definition_lower_pd below_lower_pd_def
 by (rule lower_le.typedef_ideal_po)
 
-instance lower_pd :: (sfp) cpo
+instance lower_pd :: (bifinite) cpo
 using type_definition_lower_pd below_lower_pd_def
 by (rule lower_le.typedef_ideal_cpo)
 
@@ -110,7 +110,7 @@
 lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: lower_pd.principal_induct, simp, simp)
 
-instance lower_pd :: (sfp) pcpo
+instance lower_pd :: (bifinite) pcpo
 by intro_classes (fast intro: lower_pd_minimal)
 
 lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
@@ -433,7 +433,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Lower powerdomain is an SFP domain *}
+subsection {* Lower powerdomain is a bifinite domain *}
 
 definition
   lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
@@ -463,7 +463,7 @@
 apply (erule finite_deflation_lower_map)
 done
 
-instantiation lower_pd :: (sfp) sfp
+instantiation lower_pd :: (bifinite) bifinite
 begin
 
 definition
@@ -488,8 +488,6 @@
 
 end
 
-text {* SFP of type constructor = type combinator *}
-
 lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
 by (rule sfp_lower_pd_def)
 
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Representable.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -11,23 +11,23 @@
   ("Tools/Domain/domain_isomorphism.ML")
 begin
 
-default_sort sfp
+default_sort bifinite
 
 subsection {* Representations of types *}
 
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::sfp) = cast\<cdot>SFP('a)\<cdot>x"
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
 by (simp add: cast_SFP)
 
 lemma in_SFP_iff:
-  "x ::: SFP('a::sfp) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+  "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
 by (simp add: in_sfp_def cast_SFP)
 
 lemma prj_inverse:
-  "x ::: SFP('a::sfp) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+  "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
 by (simp only: in_SFP_iff)
 
 lemma emb_in_SFP [simp]:
-  "emb\<cdot>(x::'a::sfp) ::: SFP('a)"
+  "emb\<cdot>(x::'a) ::: SFP('a)"
 by (simp add: in_SFP_iff)
 
 subsection {* Coerce operator *}
@@ -137,7 +137,7 @@
   assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
   assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
   assumes sfp: "sfp \<equiv> (\<lambda> a::'a itself. t)"
-  shows "OFCLASS('a, sfp_class)"
+  shows "OFCLASS('a, bifinite_class)"
 proof
   have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
     by (simp add: adm_in_sfp)
@@ -180,13 +180,13 @@
 text {* Restore original typing constraints *}
 
 setup {* Sign.add_const_constraint
-  (@{const_name sfp}, SOME @{typ "'a::sfp itself \<Rightarrow> sfp"}) *}
+  (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
 
 setup {* Sign.add_const_constraint
-  (@{const_name emb}, SOME @{typ "'a::sfp \<rightarrow> udom"}) *}
+  (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
 
 setup {* Sign.add_const_constraint
-  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::sfp"}) *}
+  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
 
 lemma adm_mem_Collect_in_sfp: "adm (\<lambda>x. x \<in> {x. x ::: A})"
 unfolding mem_Collect_eq by (rule adm_in_sfp)
@@ -196,7 +196,7 @@
 subsection {* Isomorphic deflations *}
 
 definition
-  isodefl :: "('a::sfp \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
+  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
 where
   "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
 
@@ -211,7 +211,7 @@
 by (drule cfun_fun_cong [where x="\<bottom>"], simp)
 
 lemma isodefl_imp_deflation:
-  fixes d :: "'a::sfp \<rightarrow> 'a"
+  fixes d :: "'a \<rightarrow> 'a"
   assumes "isodefl d t" shows "deflation d"
 proof
   note assms [unfolded isodefl_def, simp]
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -310,7 +310,7 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
-subsection {* Strict product is an SFP domain *}
+subsection {* Strict product is a bifinite domain *}
 
 definition
   sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
@@ -342,7 +342,7 @@
 apply (erule (1) finite_deflation_sprod_map)
 done
 
-instantiation sprod :: (sfp, sfp) sfp
+instantiation sprod :: (bifinite, bifinite) bifinite
 begin
 
 definition
@@ -367,9 +367,8 @@
 
 end
 
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_sprod:
+  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
 by (rule sfp_sprod_def)
 
 end
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -295,7 +295,7 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
-subsection {* Strict sum is an SFP domain *}
+subsection {* Strict sum is a bifinite domain *}
 
 definition
   ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
@@ -325,7 +325,7 @@
 apply (erule (1) finite_deflation_ssum_map)
 done
 
-instantiation ssum :: (sfp, sfp) sfp
+instantiation ssum :: (bifinite, bifinite) bifinite
 begin
 
 definition
@@ -350,9 +350,8 @@
 
 end
 
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_ssum: "SFP('a::sfp \<oplus> 'b::sfp) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_ssum:
+  "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
 by (rule sfp_ssum_def)
 
 end
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Fri Oct 08 07:39:50 2010 -0700
@@ -213,7 +213,7 @@
   end;
 
 fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
-fun rep_arg lazy = @{sort sfp};
+fun rep_arg lazy = @{sort bifinite};
 
 val add_domain =
     gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg;
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML	Fri Oct 08 07:39:50 2010 -0700
@@ -108,7 +108,7 @@
 
     (*instantiate class rep*)
     val lthy = thy
-      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort sfp});
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
     val ((_, (_, emb_ldef)), lthy) =
         Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
     val ((_, (_, prj_ldef)), lthy) =
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Tutorial/New_Domain.thy
--- a/src/HOLCF/Tutorial/New_Domain.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Tutorial/New_Domain.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -9,14 +9,14 @@
 begin
 
 text {*
-  The definitional domain package only works with SFP domains,
-  i.e. types in class @{text sfp}.
+  The definitional domain package only works with bifinite domains,
+  i.e. types in class @{text bifinite}.
 *}
 
-default_sort sfp
+default_sort bifinite
 
 text {*
-  Provided that @{text sfp} is the default sort, the @{text new_domain}
+  Provided that @{text bifinite} is the default sort, the @{text new_domain}
   package should work with any type definition supported by the old
   domain package.
 *}
diff -r 310f98585107 -r 38677db30cad src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Up.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -332,7 +332,7 @@
     by (rule finite_subset, simp add: d.finite_fixes)
 qed
 
-subsection {* Lifted cpo is an SFP domain *}
+subsection {* Lifted cpo is a bifinite domain *}
 
 definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
 where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
@@ -360,7 +360,7 @@
 apply (erule finite_deflation_u_map)
 done
 
-instantiation u :: (sfp) sfp
+instantiation u :: (bifinite) bifinite
 begin
 
 definition
@@ -385,9 +385,7 @@
 
 end
 
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_u: "SFP('a::sfp u) = u_sfp\<cdot>SFP('a)"
+lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
 by (rule sfp_u_def)
 
 end
diff -r 310f98585107 -r 38677db30cad src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -76,7 +76,7 @@
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (fast intro: upper_le.ideal_principal)
 
-instantiation upper_pd :: (sfp) below
+instantiation upper_pd :: (bifinite) below
 begin
 
 definition
@@ -85,11 +85,11 @@
 instance ..
 end
 
-instance upper_pd :: (sfp) po
+instance upper_pd :: (bifinite) po
 using type_definition_upper_pd below_upper_pd_def
 by (rule upper_le.typedef_ideal_po)
 
-instance upper_pd :: (sfp) cpo
+instance upper_pd :: (bifinite) cpo
 using type_definition_upper_pd below_upper_pd_def
 by (rule upper_le.typedef_ideal_cpo)
 
@@ -108,7 +108,7 @@
 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: upper_pd.principal_induct, simp, simp)
 
-instance upper_pd :: (sfp) pcpo
+instance upper_pd :: (bifinite) pcpo
 by intro_classes (fast intro: upper_pd_minimal)
 
 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
@@ -428,7 +428,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Upper powerdomain is an SFP domain *}
+subsection {* Upper powerdomain is a bifinite domain *}
 
 definition
   upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
@@ -458,7 +458,7 @@
 apply (erule finite_deflation_upper_map)
 done
 
-instantiation upper_pd :: (sfp) sfp
+instantiation upper_pd :: (bifinite) bifinite
 begin
 
 definition
@@ -483,8 +483,6 @@
 
 end
 
-text {* SFP of type constructor = type combinator *}
-
 lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
 by (rule sfp_upper_pd_def)
 
diff -r 310f98585107 -r 38677db30cad src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-default_sort sfp
+default_sort bifinite
 
 (*
 
@@ -93,7 +93,7 @@
 
 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
 
-instantiation foo :: (sfp) sfp
+instantiation foo :: (bifinite) bifinite
 begin
 
 definition emb_foo :: "'a foo \<rightarrow> udom"
@@ -116,7 +116,7 @@
 
 end
 
-instantiation bar :: (sfp) sfp
+instantiation bar :: (bifinite) bifinite
 begin
 
 definition emb_bar :: "'a bar \<rightarrow> udom"
@@ -139,7 +139,7 @@
 
 end
 
-instantiation baz :: (sfp) sfp
+instantiation baz :: (bifinite) bifinite
 begin
 
 definition emb_baz :: "'a baz \<rightarrow> udom"
diff -r 310f98585107 -r 38677db30cad src/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOLCF/ex/Powerdomain_ex.thy	Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/ex/Powerdomain_ex.thy	Fri Oct 08 07:39:50 2010 -0700
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-default_sort sfp
+default_sort bifinite
 
 subsection {* Monadic sorting example *}