--- 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)