rename class 'sfp' to 'bifinite'
authorhuffman
Fri Oct 08 07:39:50 2010 -0700 (2010-10-08)
changeset 3998638677db30cad
parent 39985 310f98585107
child 39987 8c2f449af35a
rename class 'sfp' to 'bifinite'
src/HOLCF/Bifinite.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cprod.thy
src/HOLCF/Library/Strict_Fun.thy
src/HOLCF/Lift.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Representable.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/repdef.ML
src/HOLCF/Tutorial/New_Domain.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
src/HOLCF/ex/Domain_Proofs.thy
src/HOLCF/ex/Powerdomain_ex.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Thu Oct 07 13:54:43 2010 -0700
     1.2 +++ b/src/HOLCF/Bifinite.thy	Fri Oct 08 07:39:50 2010 -0700
     1.3 @@ -8,14 +8,14 @@
     1.4  imports Algebraic
     1.5  begin
     1.6  
     1.7 -subsection {* Class of SFP domains *}
     1.8 +subsection {* Class of bifinite domains *}
     1.9  
    1.10  text {*
    1.11 -  We define a SFP domain as a pcpo that is isomorphic to some
    1.12 +  We define a bifinite domain as a pcpo that is isomorphic to some
    1.13    algebraic deflation over the universal domain.
    1.14  *}
    1.15  
    1.16 -class sfp = pcpo +
    1.17 +class bifinite = pcpo +
    1.18    fixes emb :: "'a::pcpo \<rightarrow> udom"
    1.19    fixes prj :: "udom \<rightarrow> 'a::pcpo"
    1.20    fixes sfp :: "'a itself \<Rightarrow> sfp"
    1.21 @@ -25,26 +25,26 @@
    1.22  syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
    1.23  translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
    1.24  
    1.25 -interpretation sfp:
    1.26 -  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
    1.27 +interpretation bifinite:
    1.28 +  pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
    1.29    unfolding pcpo_ep_pair_def
    1.30    by (rule ep_pair_emb_prj)
    1.31  
    1.32 -lemmas emb_inverse = sfp.e_inverse
    1.33 -lemmas emb_prj_below = sfp.e_p_below
    1.34 -lemmas emb_eq_iff = sfp.e_eq_iff
    1.35 -lemmas emb_strict = sfp.e_strict
    1.36 -lemmas prj_strict = sfp.p_strict
    1.37 +lemmas emb_inverse = bifinite.e_inverse
    1.38 +lemmas emb_prj_below = bifinite.e_p_below
    1.39 +lemmas emb_eq_iff = bifinite.e_eq_iff
    1.40 +lemmas emb_strict = bifinite.e_strict
    1.41 +lemmas prj_strict = bifinite.p_strict
    1.42  
    1.43 -subsection {* SFP domains have a countable compact basis *}
    1.44 +subsection {* Bifinite domains have a countable compact basis *}
    1.45  
    1.46  text {*
    1.47    Eventually it should be possible to generalize this to an unpointed
    1.48 -  variant of the sfp class.
    1.49 +  variant of the bifinite class.
    1.50  *}
    1.51  
    1.52  interpretation compact_basis:
    1.53 -  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
    1.54 +  ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
    1.55  proof -
    1.56    obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
    1.57    and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
    1.58 @@ -59,7 +59,7 @@
    1.59        by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
    1.60      show "\<And>i. finite_deflation (approx i)"
    1.61        unfolding approx_def
    1.62 -      apply (rule sfp.finite_deflation_p_d_e)
    1.63 +      apply (rule bifinite.finite_deflation_p_d_e)
    1.64        apply (rule finite_deflation_cast)
    1.65        apply (rule sfp.compact_principal)
    1.66        apply (rule below_trans [OF monofun_cfun_fun])
    1.67 @@ -146,7 +146,7 @@
    1.68  
    1.69  subsection {* Instance for universal domain type *}
    1.70  
    1.71 -instantiation udom :: sfp
    1.72 +instantiation udom :: bifinite
    1.73  begin
    1.74  
    1.75  definition [simp]:
    1.76 @@ -208,7 +208,7 @@
    1.77  apply (erule (1) finite_deflation_cfun_map)
    1.78  done
    1.79  
    1.80 -instantiation cfun :: (sfp, sfp) sfp
    1.81 +instantiation cfun :: (bifinite, bifinite) bifinite
    1.82  begin
    1.83  
    1.84  definition
    1.85 @@ -233,7 +233,8 @@
    1.86  
    1.87  end
    1.88  
    1.89 -lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.90 +lemma SFP_cfun:
    1.91 +  "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.92  by (rule sfp_cfun_def)
    1.93  
    1.94  end
     2.1 --- a/src/HOLCF/CompactBasis.thy	Thu Oct 07 13:54:43 2010 -0700
     2.2 +++ b/src/HOLCF/CompactBasis.thy	Fri Oct 08 07:39:50 2010 -0700
     2.3 @@ -8,7 +8,7 @@
     2.4  imports Bifinite
     2.5  begin
     2.6  
     2.7 -default_sort sfp
     2.8 +default_sort bifinite
     2.9  
    2.10  subsection {* A compact basis for powerdomains *}
    2.11  
    2.12 @@ -24,7 +24,7 @@
    2.13  
    2.14  text {* The powerdomain basis type is countable. *}
    2.15  
    2.16 -lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f"
    2.17 +lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
    2.18  proof -
    2.19    obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
    2.20      using compact_basis.countable ..
     3.1 --- a/src/HOLCF/ConvexPD.thy	Thu Oct 07 13:54:43 2010 -0700
     3.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Oct 08 07:39:50 2010 -0700
     3.3 @@ -123,7 +123,7 @@
     3.4    "{S::'a pd_basis set. convex_le.ideal S}"
     3.5  by (fast intro: convex_le.ideal_principal)
     3.6  
     3.7 -instantiation convex_pd :: (sfp) below
     3.8 +instantiation convex_pd :: (bifinite) below
     3.9  begin
    3.10  
    3.11  definition
    3.12 @@ -132,11 +132,11 @@
    3.13  instance ..
    3.14  end
    3.15  
    3.16 -instance convex_pd :: (sfp) po
    3.17 +instance convex_pd :: (bifinite) po
    3.18  using type_definition_convex_pd below_convex_pd_def
    3.19  by (rule convex_le.typedef_ideal_po)
    3.20  
    3.21 -instance convex_pd :: (sfp) cpo
    3.22 +instance convex_pd :: (bifinite) cpo
    3.23  using type_definition_convex_pd below_convex_pd_def
    3.24  by (rule convex_le.typedef_ideal_cpo)
    3.25  
    3.26 @@ -155,7 +155,7 @@
    3.27  lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    3.28  by (induct ys rule: convex_pd.principal_induct, simp, simp)
    3.29  
    3.30 -instance convex_pd :: (sfp) pcpo
    3.31 +instance convex_pd :: (bifinite) pcpo
    3.32  by intro_classes (fast intro: convex_pd_minimal)
    3.33  
    3.34  lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
    3.35 @@ -444,7 +444,7 @@
    3.36      by (rule finite_range_imp_finite_fixes)
    3.37  qed
    3.38  
    3.39 -subsection {* Convex powerdomain is an SFP domain *}
    3.40 +subsection {* Convex powerdomain is a bifinite domain *}
    3.41  
    3.42  definition
    3.43    convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
    3.44 @@ -474,7 +474,7 @@
    3.45  apply (erule finite_deflation_convex_map)
    3.46  done
    3.47  
    3.48 -instantiation convex_pd :: (sfp) sfp
    3.49 +instantiation convex_pd :: (bifinite) bifinite
    3.50  begin
    3.51  
    3.52  definition
     4.1 --- a/src/HOLCF/Cprod.thy	Thu Oct 07 13:54:43 2010 -0700
     4.2 +++ b/src/HOLCF/Cprod.thy	Fri Oct 08 07:39:50 2010 -0700
     4.3 @@ -97,7 +97,7 @@
     4.4      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
     4.5  qed
     4.6  
     4.7 -subsection {* Cartesian product is an SFP domain *}
     4.8 +subsection {* Cartesian product is a bifinite domain *}
     4.9  
    4.10  definition
    4.11    prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
    4.12 @@ -127,7 +127,7 @@
    4.13  apply (erule (1) finite_deflation_cprod_map)
    4.14  done
    4.15  
    4.16 -instantiation prod :: (sfp, sfp) sfp
    4.17 +instantiation prod :: (bifinite, bifinite) bifinite
    4.18  begin
    4.19  
    4.20  definition
    4.21 @@ -152,7 +152,8 @@
    4.22  
    4.23  end
    4.24  
    4.25 -lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    4.26 +lemma SFP_prod:
    4.27 +  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    4.28  by (rule sfp_prod_def)
    4.29  
    4.30  end
     5.1 --- a/src/HOLCF/Library/Strict_Fun.thy	Thu Oct 07 13:54:43 2010 -0700
     5.2 +++ b/src/HOLCF/Library/Strict_Fun.thy	Fri Oct 08 07:39:50 2010 -0700
     5.3 @@ -143,7 +143,7 @@
     5.4           deflation_strict `deflation d1` `deflation d2`)
     5.5  qed
     5.6  
     5.7 -subsection {* Strict function space is an SFP domain *}
     5.8 +subsection {* Strict function space is a bifinite domain *}
     5.9  
    5.10  definition
    5.11    sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
    5.12 @@ -173,7 +173,7 @@
    5.13  apply (erule (1) finite_deflation_sfun_map)
    5.14  done
    5.15  
    5.16 -instantiation sfun :: (sfp, sfp) sfp
    5.17 +instantiation sfun :: (bifinite, bifinite) bifinite
    5.18  begin
    5.19  
    5.20  definition
    5.21 @@ -198,9 +198,8 @@
    5.22  
    5.23  end
    5.24  
    5.25 -text {* SFP of type constructor = type combinator *}
    5.26 -
    5.27 -lemma SFP_sfun: "SFP('a::sfp \<rightarrow>! 'b::sfp) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    5.28 +lemma SFP_sfun:
    5.29 +  "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    5.30  by (rule sfp_sfun_def)
    5.31  
    5.32  lemma isodefl_sfun:
     6.1 --- a/src/HOLCF/Lift.thy	Thu Oct 07 13:54:43 2010 -0700
     6.2 +++ b/src/HOLCF/Lift.thy	Fri Oct 08 07:39:50 2010 -0700
     6.3 @@ -171,7 +171,7 @@
     6.4  by (cases x, simp_all)
     6.5  
     6.6  
     6.7 -subsection {* Lifted countable types are SFP domains *}
     6.8 +subsection {* Lifted countable types are bifinite domains *}
     6.9  
    6.10  definition
    6.11    lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
    6.12 @@ -220,7 +220,7 @@
    6.13  using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
    6.14  by (rule approx_chain.intro)
    6.15  
    6.16 -instantiation lift :: (countable) sfp
    6.17 +instantiation lift :: (countable) bifinite
    6.18  begin
    6.19  
    6.20  definition
     7.1 --- a/src/HOLCF/LowerPD.thy	Thu Oct 07 13:54:43 2010 -0700
     7.2 +++ b/src/HOLCF/LowerPD.thy	Fri Oct 08 07:39:50 2010 -0700
     7.3 @@ -78,7 +78,7 @@
     7.4    "{S::'a pd_basis set. lower_le.ideal S}"
     7.5  by (fast intro: lower_le.ideal_principal)
     7.6  
     7.7 -instantiation lower_pd :: (sfp) below
     7.8 +instantiation lower_pd :: (bifinite) below
     7.9  begin
    7.10  
    7.11  definition
    7.12 @@ -87,11 +87,11 @@
    7.13  instance ..
    7.14  end
    7.15  
    7.16 -instance lower_pd :: (sfp) po
    7.17 +instance lower_pd :: (bifinite) po
    7.18  using type_definition_lower_pd below_lower_pd_def
    7.19  by (rule lower_le.typedef_ideal_po)
    7.20  
    7.21 -instance lower_pd :: (sfp) cpo
    7.22 +instance lower_pd :: (bifinite) cpo
    7.23  using type_definition_lower_pd below_lower_pd_def
    7.24  by (rule lower_le.typedef_ideal_cpo)
    7.25  
    7.26 @@ -110,7 +110,7 @@
    7.27  lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    7.28  by (induct ys rule: lower_pd.principal_induct, simp, simp)
    7.29  
    7.30 -instance lower_pd :: (sfp) pcpo
    7.31 +instance lower_pd :: (bifinite) pcpo
    7.32  by intro_classes (fast intro: lower_pd_minimal)
    7.33  
    7.34  lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
    7.35 @@ -433,7 +433,7 @@
    7.36      by (rule finite_range_imp_finite_fixes)
    7.37  qed
    7.38  
    7.39 -subsection {* Lower powerdomain is an SFP domain *}
    7.40 +subsection {* Lower powerdomain is a bifinite domain *}
    7.41  
    7.42  definition
    7.43    lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
    7.44 @@ -463,7 +463,7 @@
    7.45  apply (erule finite_deflation_lower_map)
    7.46  done
    7.47  
    7.48 -instantiation lower_pd :: (sfp) sfp
    7.49 +instantiation lower_pd :: (bifinite) bifinite
    7.50  begin
    7.51  
    7.52  definition
    7.53 @@ -488,8 +488,6 @@
    7.54  
    7.55  end
    7.56  
    7.57 -text {* SFP of type constructor = type combinator *}
    7.58 -
    7.59  lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
    7.60  by (rule sfp_lower_pd_def)
    7.61  
     8.1 --- a/src/HOLCF/Representable.thy	Thu Oct 07 13:54:43 2010 -0700
     8.2 +++ b/src/HOLCF/Representable.thy	Fri Oct 08 07:39:50 2010 -0700
     8.3 @@ -11,23 +11,23 @@
     8.4    ("Tools/Domain/domain_isomorphism.ML")
     8.5  begin
     8.6  
     8.7 -default_sort sfp
     8.8 +default_sort bifinite
     8.9  
    8.10  subsection {* Representations of types *}
    8.11  
    8.12 -lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::sfp) = cast\<cdot>SFP('a)\<cdot>x"
    8.13 +lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
    8.14  by (simp add: cast_SFP)
    8.15  
    8.16  lemma in_SFP_iff:
    8.17 -  "x ::: SFP('a::sfp) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    8.18 +  "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    8.19  by (simp add: in_sfp_def cast_SFP)
    8.20  
    8.21  lemma prj_inverse:
    8.22 -  "x ::: SFP('a::sfp) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    8.23 +  "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    8.24  by (simp only: in_SFP_iff)
    8.25  
    8.26  lemma emb_in_SFP [simp]:
    8.27 -  "emb\<cdot>(x::'a::sfp) ::: SFP('a)"
    8.28 +  "emb\<cdot>(x::'a) ::: SFP('a)"
    8.29  by (simp add: in_SFP_iff)
    8.30  
    8.31  subsection {* Coerce operator *}
    8.32 @@ -137,7 +137,7 @@
    8.33    assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
    8.34    assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
    8.35    assumes sfp: "sfp \<equiv> (\<lambda> a::'a itself. t)"
    8.36 -  shows "OFCLASS('a, sfp_class)"
    8.37 +  shows "OFCLASS('a, bifinite_class)"
    8.38  proof
    8.39    have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
    8.40      by (simp add: adm_in_sfp)
    8.41 @@ -180,13 +180,13 @@
    8.42  text {* Restore original typing constraints *}
    8.43  
    8.44  setup {* Sign.add_const_constraint
    8.45 -  (@{const_name sfp}, SOME @{typ "'a::sfp itself \<Rightarrow> sfp"}) *}
    8.46 +  (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
    8.47  
    8.48  setup {* Sign.add_const_constraint
    8.49 -  (@{const_name emb}, SOME @{typ "'a::sfp \<rightarrow> udom"}) *}
    8.50 +  (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
    8.51  
    8.52  setup {* Sign.add_const_constraint
    8.53 -  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::sfp"}) *}
    8.54 +  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
    8.55  
    8.56  lemma adm_mem_Collect_in_sfp: "adm (\<lambda>x. x \<in> {x. x ::: A})"
    8.57  unfolding mem_Collect_eq by (rule adm_in_sfp)
    8.58 @@ -196,7 +196,7 @@
    8.59  subsection {* Isomorphic deflations *}
    8.60  
    8.61  definition
    8.62 -  isodefl :: "('a::sfp \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
    8.63 +  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
    8.64  where
    8.65    "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
    8.66  
    8.67 @@ -211,7 +211,7 @@
    8.68  by (drule cfun_fun_cong [where x="\<bottom>"], simp)
    8.69  
    8.70  lemma isodefl_imp_deflation:
    8.71 -  fixes d :: "'a::sfp \<rightarrow> 'a"
    8.72 +  fixes d :: "'a \<rightarrow> 'a"
    8.73    assumes "isodefl d t" shows "deflation d"
    8.74  proof
    8.75    note assms [unfolded isodefl_def, simp]
     9.1 --- a/src/HOLCF/Sprod.thy	Thu Oct 07 13:54:43 2010 -0700
     9.2 +++ b/src/HOLCF/Sprod.thy	Fri Oct 08 07:39:50 2010 -0700
     9.3 @@ -310,7 +310,7 @@
     9.4      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
     9.5  qed
     9.6  
     9.7 -subsection {* Strict product is an SFP domain *}
     9.8 +subsection {* Strict product is a bifinite domain *}
     9.9  
    9.10  definition
    9.11    sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    9.12 @@ -342,7 +342,7 @@
    9.13  apply (erule (1) finite_deflation_sprod_map)
    9.14  done
    9.15  
    9.16 -instantiation sprod :: (sfp, sfp) sfp
    9.17 +instantiation sprod :: (bifinite, bifinite) bifinite
    9.18  begin
    9.19  
    9.20  definition
    9.21 @@ -367,9 +367,8 @@
    9.22  
    9.23  end
    9.24  
    9.25 -text {* SFP of type constructor = type combinator *}
    9.26 -
    9.27 -lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    9.28 +lemma SFP_sprod:
    9.29 +  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    9.30  by (rule sfp_sprod_def)
    9.31  
    9.32  end
    10.1 --- a/src/HOLCF/Ssum.thy	Thu Oct 07 13:54:43 2010 -0700
    10.2 +++ b/src/HOLCF/Ssum.thy	Fri Oct 08 07:39:50 2010 -0700
    10.3 @@ -295,7 +295,7 @@
    10.4      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    10.5  qed
    10.6  
    10.7 -subsection {* Strict sum is an SFP domain *}
    10.8 +subsection {* Strict sum is a bifinite domain *}
    10.9  
   10.10  definition
   10.11    ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
   10.12 @@ -325,7 +325,7 @@
   10.13  apply (erule (1) finite_deflation_ssum_map)
   10.14  done
   10.15  
   10.16 -instantiation ssum :: (sfp, sfp) sfp
   10.17 +instantiation ssum :: (bifinite, bifinite) bifinite
   10.18  begin
   10.19  
   10.20  definition
   10.21 @@ -350,9 +350,8 @@
   10.22  
   10.23  end
   10.24  
   10.25 -text {* SFP of type constructor = type combinator *}
   10.26 -
   10.27 -lemma SFP_ssum: "SFP('a::sfp \<oplus> 'b::sfp) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   10.28 +lemma SFP_ssum:
   10.29 +  "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   10.30  by (rule sfp_ssum_def)
   10.31  
   10.32  end
    11.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 07 13:54:43 2010 -0700
    11.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Fri Oct 08 07:39:50 2010 -0700
    11.3 @@ -213,7 +213,7 @@
    11.4    end;
    11.5  
    11.6  fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
    11.7 -fun rep_arg lazy = @{sort sfp};
    11.8 +fun rep_arg lazy = @{sort bifinite};
    11.9  
   11.10  val add_domain =
   11.11      gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg;
    12.1 --- a/src/HOLCF/Tools/repdef.ML	Thu Oct 07 13:54:43 2010 -0700
    12.2 +++ b/src/HOLCF/Tools/repdef.ML	Fri Oct 08 07:39:50 2010 -0700
    12.3 @@ -108,7 +108,7 @@
    12.4  
    12.5      (*instantiate class rep*)
    12.6      val lthy = thy
    12.7 -      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort sfp});
    12.8 +      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
    12.9      val ((_, (_, emb_ldef)), lthy) =
   12.10          Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
   12.11      val ((_, (_, prj_ldef)), lthy) =
    13.1 --- a/src/HOLCF/Tutorial/New_Domain.thy	Thu Oct 07 13:54:43 2010 -0700
    13.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Fri Oct 08 07:39:50 2010 -0700
    13.3 @@ -9,14 +9,14 @@
    13.4  begin
    13.5  
    13.6  text {*
    13.7 -  The definitional domain package only works with SFP domains,
    13.8 -  i.e. types in class @{text sfp}.
    13.9 +  The definitional domain package only works with bifinite domains,
   13.10 +  i.e. types in class @{text bifinite}.
   13.11  *}
   13.12  
   13.13 -default_sort sfp
   13.14 +default_sort bifinite
   13.15  
   13.16  text {*
   13.17 -  Provided that @{text sfp} is the default sort, the @{text new_domain}
   13.18 +  Provided that @{text bifinite} is the default sort, the @{text new_domain}
   13.19    package should work with any type definition supported by the old
   13.20    domain package.
   13.21  *}
    14.1 --- a/src/HOLCF/Up.thy	Thu Oct 07 13:54:43 2010 -0700
    14.2 +++ b/src/HOLCF/Up.thy	Fri Oct 08 07:39:50 2010 -0700
    14.3 @@ -332,7 +332,7 @@
    14.4      by (rule finite_subset, simp add: d.finite_fixes)
    14.5  qed
    14.6  
    14.7 -subsection {* Lifted cpo is an SFP domain *}
    14.8 +subsection {* Lifted cpo is a bifinite domain *}
    14.9  
   14.10  definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
   14.11  where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
   14.12 @@ -360,7 +360,7 @@
   14.13  apply (erule finite_deflation_u_map)
   14.14  done
   14.15  
   14.16 -instantiation u :: (sfp) sfp
   14.17 +instantiation u :: (bifinite) bifinite
   14.18  begin
   14.19  
   14.20  definition
   14.21 @@ -385,9 +385,7 @@
   14.22  
   14.23  end
   14.24  
   14.25 -text {* SFP of type constructor = type combinator *}
   14.26 -
   14.27 -lemma SFP_u: "SFP('a::sfp u) = u_sfp\<cdot>SFP('a)"
   14.28 +lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
   14.29  by (rule sfp_u_def)
   14.30  
   14.31  end
    15.1 --- a/src/HOLCF/UpperPD.thy	Thu Oct 07 13:54:43 2010 -0700
    15.2 +++ b/src/HOLCF/UpperPD.thy	Fri Oct 08 07:39:50 2010 -0700
    15.3 @@ -76,7 +76,7 @@
    15.4    "{S::'a pd_basis set. upper_le.ideal S}"
    15.5  by (fast intro: upper_le.ideal_principal)
    15.6  
    15.7 -instantiation upper_pd :: (sfp) below
    15.8 +instantiation upper_pd :: (bifinite) below
    15.9  begin
   15.10  
   15.11  definition
   15.12 @@ -85,11 +85,11 @@
   15.13  instance ..
   15.14  end
   15.15  
   15.16 -instance upper_pd :: (sfp) po
   15.17 +instance upper_pd :: (bifinite) po
   15.18  using type_definition_upper_pd below_upper_pd_def
   15.19  by (rule upper_le.typedef_ideal_po)
   15.20  
   15.21 -instance upper_pd :: (sfp) cpo
   15.22 +instance upper_pd :: (bifinite) cpo
   15.23  using type_definition_upper_pd below_upper_pd_def
   15.24  by (rule upper_le.typedef_ideal_cpo)
   15.25  
   15.26 @@ -108,7 +108,7 @@
   15.27  lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   15.28  by (induct ys rule: upper_pd.principal_induct, simp, simp)
   15.29  
   15.30 -instance upper_pd :: (sfp) pcpo
   15.31 +instance upper_pd :: (bifinite) pcpo
   15.32  by intro_classes (fast intro: upper_pd_minimal)
   15.33  
   15.34  lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
   15.35 @@ -428,7 +428,7 @@
   15.36      by (rule finite_range_imp_finite_fixes)
   15.37  qed
   15.38  
   15.39 -subsection {* Upper powerdomain is an SFP domain *}
   15.40 +subsection {* Upper powerdomain is a bifinite domain *}
   15.41  
   15.42  definition
   15.43    upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
   15.44 @@ -458,7 +458,7 @@
   15.45  apply (erule finite_deflation_upper_map)
   15.46  done
   15.47  
   15.48 -instantiation upper_pd :: (sfp) sfp
   15.49 +instantiation upper_pd :: (bifinite) bifinite
   15.50  begin
   15.51  
   15.52  definition
   15.53 @@ -483,8 +483,6 @@
   15.54  
   15.55  end
   15.56  
   15.57 -text {* SFP of type constructor = type combinator *}
   15.58 -
   15.59  lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
   15.60  by (rule sfp_upper_pd_def)
   15.61  
    16.1 --- a/src/HOLCF/ex/Domain_Proofs.thy	Thu Oct 07 13:54:43 2010 -0700
    16.2 +++ b/src/HOLCF/ex/Domain_Proofs.thy	Fri Oct 08 07:39:50 2010 -0700
    16.3 @@ -8,7 +8,7 @@
    16.4  imports HOLCF
    16.5  begin
    16.6  
    16.7 -default_sort sfp
    16.8 +default_sort bifinite
    16.9  
   16.10  (*
   16.11  
   16.12 @@ -93,7 +93,7 @@
   16.13  
   16.14  text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
   16.15  
   16.16 -instantiation foo :: (sfp) sfp
   16.17 +instantiation foo :: (bifinite) bifinite
   16.18  begin
   16.19  
   16.20  definition emb_foo :: "'a foo \<rightarrow> udom"
   16.21 @@ -116,7 +116,7 @@
   16.22  
   16.23  end
   16.24  
   16.25 -instantiation bar :: (sfp) sfp
   16.26 +instantiation bar :: (bifinite) bifinite
   16.27  begin
   16.28  
   16.29  definition emb_bar :: "'a bar \<rightarrow> udom"
   16.30 @@ -139,7 +139,7 @@
   16.31  
   16.32  end
   16.33  
   16.34 -instantiation baz :: (sfp) sfp
   16.35 +instantiation baz :: (bifinite) bifinite
   16.36  begin
   16.37  
   16.38  definition emb_baz :: "'a baz \<rightarrow> udom"
    17.1 --- a/src/HOLCF/ex/Powerdomain_ex.thy	Thu Oct 07 13:54:43 2010 -0700
    17.2 +++ b/src/HOLCF/ex/Powerdomain_ex.thy	Fri Oct 08 07:39:50 2010 -0700
    17.3 @@ -8,7 +8,7 @@
    17.4  imports HOLCF
    17.5  begin
    17.6  
    17.7 -default_sort sfp
    17.8 +default_sort bifinite
    17.9  
   17.10  subsection {* Monadic sorting example *}
   17.11