# HG changeset patch
# User huffman
# Date 1286811129 25200
# Node ID ad60d7311f4360954f62b96e1e79aca591c9fa81
# Parent  a4b2971952f46898ca0b800685d575378da0a447
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)

diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -72,36 +72,29 @@
 
 subsection {* Defining algebraic deflations by ideal completion *}
 
-text {*
-  An SFP domain is one that can be represented as the limit of a
-  sequence of finite posets.  Here we use omega-algebraic deflations
-  (i.e. countable ideals of finite deflations) to model sequences of
-  finite posets.
-*}
-
-typedef (open) sfp = "{S::fin_defl set. below.ideal S}"
+typedef (open) defl = "{S::fin_defl set. below.ideal S}"
 by (fast intro: below.ideal_principal)
 
-instantiation sfp :: below
+instantiation defl :: below
 begin
 
 definition
-  "x \<sqsubseteq> y \<longleftrightarrow> Rep_sfp x \<subseteq> Rep_sfp y"
+  "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
 
 instance ..
 end
 
-instance sfp :: po
-using type_definition_sfp below_sfp_def
+instance defl :: po
+using type_definition_defl below_defl_def
 by (rule below.typedef_ideal_po)
 
-instance sfp :: cpo
-using type_definition_sfp below_sfp_def
+instance defl :: cpo
+using type_definition_defl below_defl_def
 by (rule below.typedef_ideal_cpo)
 
 definition
-  sfp_principal :: "fin_defl \<Rightarrow> sfp" where
-  "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
+  defl_principal :: "fin_defl \<Rightarrow> defl" where
+  "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
 
 lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
 proof
@@ -130,52 +123,52 @@
     done
 qed
 
-interpretation sfp: ideal_completion below sfp_principal Rep_sfp
-using type_definition_sfp below_sfp_def
-using sfp_principal_def fin_defl_countable
+interpretation defl: ideal_completion below defl_principal Rep_defl
+using type_definition_defl below_defl_def
+using defl_principal_def fin_defl_countable
 by (rule below.typedef_ideal_completion)
 
 text {* Algebraic deflations are pointed *}
 
-lemma sfp_minimal: "sfp_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
-apply (induct x rule: sfp.principal_induct, simp)
-apply (rule sfp.principal_mono)
+lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
+apply (induct x rule: defl.principal_induct, simp)
+apply (rule defl.principal_mono)
 apply (simp add: below_fin_defl_def)
 apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
 done
 
-instance sfp :: pcpo
-by intro_classes (fast intro: sfp_minimal)
+instance defl :: pcpo
+by intro_classes (fast intro: defl_minimal)
 
-lemma inst_sfp_pcpo: "\<bottom> = sfp_principal (Abs_fin_defl \<bottom>)"
-by (rule sfp_minimal [THEN UU_I, symmetric])
+lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
+by (rule defl_minimal [THEN UU_I, symmetric])
 
 subsection {* Applying algebraic deflations *}
 
 definition
-  cast :: "sfp \<rightarrow> udom \<rightarrow> udom"
+  cast :: "defl \<rightarrow> udom \<rightarrow> udom"
 where
-  "cast = sfp.basis_fun Rep_fin_defl"
+  "cast = defl.basis_fun Rep_fin_defl"
 
-lemma cast_sfp_principal:
-  "cast\<cdot>(sfp_principal a) = Rep_fin_defl a"
+lemma cast_defl_principal:
+  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
 unfolding cast_def
-apply (rule sfp.basis_fun_principal)
+apply (rule defl.basis_fun_principal)
 apply (simp only: below_fin_defl_def)
 done
 
 lemma deflation_cast: "deflation (cast\<cdot>d)"
-apply (induct d rule: sfp.principal_induct)
+apply (induct d rule: defl.principal_induct)
 apply (rule adm_subst [OF _ adm_deflation], simp)
-apply (simp add: cast_sfp_principal)
+apply (simp add: cast_defl_principal)
 apply (rule finite_deflation_imp_deflation)
 apply (rule finite_deflation_Rep_fin_defl)
 done
 
 lemma finite_deflation_cast:
   "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
-apply (drule sfp.compact_imp_principal, clarify)
-apply (simp add: cast_sfp_principal)
+apply (drule defl.compact_imp_principal, clarify)
+apply (simp add: cast_defl_principal)
 apply (rule finite_deflation_Rep_fin_defl)
 done
 
@@ -190,9 +183,9 @@
 done
 
 lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
-apply (induct A rule: sfp.principal_induct, simp)
-apply (induct B rule: sfp.principal_induct, simp)
-apply (simp add: cast_sfp_principal below_fin_defl_def)
+apply (induct A rule: defl.principal_induct, simp)
+apply (induct B rule: defl.principal_induct, simp)
+apply (simp add: cast_defl_principal below_fin_defl_def)
 done
 
 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
@@ -209,8 +202,8 @@
 by (simp add: below_antisym cast_below_imp_below)
 
 lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
-apply (subst inst_sfp_pcpo)
-apply (subst cast_sfp_principal)
+apply (subst inst_defl_pcpo)
+apply (subst cast_defl_principal)
 apply (rule Abs_fin_defl_inverse)
 apply (simp add: finite_deflation_UU)
 done
@@ -221,40 +214,40 @@
 subsection {* Deflation membership relation *}
 
 definition
-  in_sfp :: "udom \<Rightarrow> sfp \<Rightarrow> bool" (infixl ":::" 50)
+  in_defl :: "udom \<Rightarrow> defl \<Rightarrow> bool" (infixl ":::" 50)
 where
   "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
 
-lemma adm_in_sfp: "adm (\<lambda>x. x ::: A)"
-unfolding in_sfp_def by simp
+lemma adm_in_defl: "adm (\<lambda>x. x ::: A)"
+unfolding in_defl_def by simp
 
-lemma in_sfpI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
-unfolding in_sfp_def .
+lemma in_deflI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
+unfolding in_defl_def .
 
 lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
-unfolding in_sfp_def .
+unfolding in_defl_def .
 
-lemma cast_in_sfp [simp]: "cast\<cdot>A\<cdot>x ::: A"
-unfolding in_sfp_def by (rule cast.idem)
+lemma cast_in_defl [simp]: "cast\<cdot>A\<cdot>x ::: A"
+unfolding in_defl_def by (rule cast.idem)
 
-lemma bottom_in_sfp [simp]: "\<bottom> ::: A"
-unfolding in_sfp_def by (rule cast_strict2)
+lemma bottom_in_defl [simp]: "\<bottom> ::: A"
+unfolding in_defl_def by (rule cast_strict2)
 
-lemma sfp_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
-unfolding in_sfp_def
+lemma defl_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
+unfolding in_defl_def
  apply (rule deflation.belowD)
    apply (rule deflation_cast)
   apply (erule monofun_cfun_arg)
  apply assumption
 done
 
-lemma rev_sfp_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
-by (rule sfp_belowD)
+lemma rev_defl_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
+by (rule defl_belowD)
 
-lemma sfp_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
+lemma defl_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
 apply (rule cast_below_imp_below)
 apply (rule cast.belowI)
-apply (simp add: in_sfp_def)
+apply (simp add: in_defl_def)
 done
 
 end
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Bifinite.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -18,12 +18,12 @@
 class bifinite = pcpo +
   fixes emb :: "'a::pcpo \<rightarrow> udom"
   fixes prj :: "udom \<rightarrow> 'a::pcpo"
-  fixes sfp :: "'a itself \<Rightarrow> sfp"
+  fixes defl :: "'a itself \<Rightarrow> defl"
   assumes ep_pair_emb_prj: "ep_pair emb prj"
-  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
+  assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
 
-syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
-translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
+syntax "_DEFL" :: "type \<Rightarrow> defl"  ("(1DEFL/(1'(_')))")
+translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
 
 interpretation bifinite:
   pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
@@ -47,24 +47,24 @@
   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))"
-    by (rule sfp.obtain_principal_chain)
-  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
-  interpret sfp_approx: approx_chain approx
+  and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
+    by (rule defl.obtain_principal_chain)
+  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
+  interpret defl_approx: approx_chain approx
   proof (rule approx_chain.intro)
     show "chain (\<lambda>i. approx i)"
       unfolding approx_def by (simp add: Y)
     show "(\<Squnion>i. approx i) = ID"
       unfolding approx_def
-      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
+      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq)
     show "\<And>i. finite_deflation (approx i)"
       unfolding approx_def
       apply (rule bifinite.finite_deflation_p_d_e)
       apply (rule finite_deflation_cast)
-      apply (rule sfp.compact_principal)
+      apply (rule defl.compact_principal)
       apply (rule below_trans [OF monofun_cfun_fun])
       apply (rule is_ub_thelub, simp add: Y)
-      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
+      apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL)
       done
   qed
   (* FIXME: why does show ?thesis fail here? *)
@@ -74,30 +74,30 @@
 subsection {* Type combinators *}
 
 definition
-  sfp_fun1 ::
-    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
+  defl_fun1 ::
+    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
 where
-  "sfp_fun1 approx f =
-    sfp.basis_fun (\<lambda>a.
-      sfp_principal (Abs_fin_defl
+  "defl_fun1 approx f =
+    defl.basis_fun (\<lambda>a.
+      defl_principal (Abs_fin_defl
         (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
 
 definition
-  sfp_fun2 ::
+  defl_fun2 ::
     "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
-      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
+      \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)"
 where
-  "sfp_fun2 approx f =
-    sfp.basis_fun (\<lambda>a.
-      sfp.basis_fun (\<lambda>b.
-        sfp_principal (Abs_fin_defl
+  "defl_fun2 approx f =
+    defl.basis_fun (\<lambda>a.
+      defl.basis_fun (\<lambda>b.
+        defl_principal (Abs_fin_defl
           (udom_emb approx oo
             f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
 
-lemma cast_sfp_fun1:
+lemma cast_defl_fun1:
   assumes approx: "approx_chain approx"
   assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
-  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
+  shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
 proof -
   have 1: "\<And>a. finite_deflation
         (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
@@ -106,23 +106,23 @@
     apply (rule f, rule finite_deflation_Rep_fin_defl)
     done
   show ?thesis
-    by (induct A rule: sfp.principal_induct, simp)
-       (simp only: sfp_fun1_def
-                   sfp.basis_fun_principal
-                   sfp.basis_fun_mono
-                   sfp.principal_mono
+    by (induct A rule: defl.principal_induct, simp)
+       (simp only: defl_fun1_def
+                   defl.basis_fun_principal
+                   defl.basis_fun_mono
+                   defl.principal_mono
                    Abs_fin_defl_mono [OF 1 1]
                    monofun_cfun below_refl
                    Rep_fin_defl_mono
-                   cast_sfp_principal
+                   cast_defl_principal
                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
 qed
 
-lemma cast_sfp_fun2:
+lemma cast_defl_fun2:
   assumes approx: "approx_chain approx"
   assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
                 finite_deflation (f\<cdot>a\<cdot>b)"
-  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
+  shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) =
     udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
 proof -
   have 1: "\<And>a b. finite_deflation (udom_emb approx oo
@@ -132,15 +132,15 @@
     apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
     done
   show ?thesis
-    by (induct A B rule: sfp.principal_induct2, simp, simp)
-       (simp only: sfp_fun2_def
-                   sfp.basis_fun_principal
-                   sfp.basis_fun_mono
-                   sfp.principal_mono
+    by (induct A B rule: defl.principal_induct2, simp, simp)
+       (simp only: defl_fun2_def
+                   defl.basis_fun_principal
+                   defl.basis_fun_mono
+                   defl.principal_mono
                    Abs_fin_defl_mono [OF 1 1]
                    monofun_cfun below_refl
                    Rep_fin_defl_mono
-                   cast_sfp_principal
+                   cast_defl_principal
                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
 qed
 
@@ -156,22 +156,22 @@
   "prj = (ID :: udom \<rightarrow> udom)"
 
 definition
-  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
+  "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> udom)"
     by (simp add: ep_pair.intro)
 next
-  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
-    unfolding sfp_udom_def
+  show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
+    unfolding defl_udom_def
     apply (subst contlub_cfun_arg)
     apply (rule chainI)
-    apply (rule sfp.principal_mono)
+    apply (rule defl.principal_mono)
     apply (simp add: below_fin_defl_def)
     apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
     apply (rule chainE)
     apply (rule chain_udom_approx)
-    apply (subst cast_sfp_principal)
+    apply (subst cast_defl_principal)
     apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
     done
 qed
@@ -197,14 +197,14 @@
     by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
 qed
 
-definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
+definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "cfun_defl = defl_fun2 cfun_approx cfun_map"
 
-lemma cast_cfun_sfp:
-  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
+lemma cast_cfun_defl:
+  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
     udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
-unfolding cfun_sfp_def
-apply (rule cast_sfp_fun2 [OF cfun_approx])
+unfolding cfun_defl_def
+apply (rule cast_defl_fun2 [OF cfun_approx])
 apply (erule (1) finite_deflation_cfun_map)
 done
 
@@ -218,7 +218,7 @@
   "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
 
 definition
-  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+  "defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
@@ -226,16 +226,16 @@
     using ep_pair_udom [OF cfun_approx]
     by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
-    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
+  show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
+    unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map)
 qed
 
 end
 
-lemma SFP_cfun:
-  "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_cfun_def)
+lemma DEFL_cfun:
+  "DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_cfun_def)
 
 subsection {* Cartesian product is a bifinite domain *}
 
@@ -256,14 +256,14 @@
     by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
 qed
 
-definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "prod_sfp = sfp_fun2 prod_approx cprod_map"
+definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "prod_defl = defl_fun2 prod_approx cprod_map"
 
-lemma cast_prod_sfp:
-  "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
+lemma cast_prod_defl:
+  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
     cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
-unfolding prod_sfp_def
-apply (rule cast_sfp_fun2 [OF prod_approx])
+unfolding prod_defl_def
+apply (rule cast_defl_fun2 [OF prod_approx])
 apply (erule (1) finite_deflation_cprod_map)
 done
 
@@ -277,7 +277,7 @@
   "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
 
 definition
-  "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+  "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
@@ -285,16 +285,16 @@
     using ep_pair_udom [OF prod_approx]
     by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
-    unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
+  show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+    unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map)
 qed
 
 end
 
-lemma SFP_prod:
-  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_prod_def)
+lemma DEFL_prod:
+  "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_prod_def)
 
 subsection {* Strict product is a bifinite domain *}
 
@@ -315,16 +315,16 @@
     by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
 qed
 
-definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
+definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "sprod_defl = defl_fun2 sprod_approx sprod_map"
 
-lemma cast_sprod_sfp:
-  "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
+lemma cast_sprod_defl:
+  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
     udom_emb sprod_approx oo
       sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
         udom_prj sprod_approx"
-unfolding sprod_sfp_def
-apply (rule cast_sfp_fun2 [OF sprod_approx])
+unfolding sprod_defl_def
+apply (rule cast_defl_fun2 [OF sprod_approx])
 apply (erule (1) finite_deflation_sprod_map)
 done
 
@@ -338,7 +338,7 @@
   "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
 
 definition
-  "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+  "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
@@ -346,16 +346,16 @@
     using ep_pair_udom [OF sprod_approx]
     by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
-    unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
+  show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+    unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map)
 qed
 
 end
 
-lemma SFP_sprod:
-  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_sprod_def)
+lemma DEFL_sprod:
+  "DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sprod_def)
 
 subsection {* Lifted cpo is a bifinite domain *}
 
@@ -374,14 +374,14 @@
     by (intro finite_deflation_u_map finite_deflation_udom_approx)
 qed
 
-definition u_sfp :: "sfp \<rightarrow> sfp"
-where "u_sfp = sfp_fun1 u_approx u_map"
+definition u_defl :: "defl \<rightarrow> defl"
+where "u_defl = defl_fun1 u_approx u_map"
 
-lemma cast_u_sfp:
-  "cast\<cdot>(u_sfp\<cdot>A) =
+lemma cast_u_defl:
+  "cast\<cdot>(u_defl\<cdot>A) =
     udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
-unfolding u_sfp_def
-apply (rule cast_sfp_fun1 [OF u_approx])
+unfolding u_defl_def
+apply (rule cast_defl_fun1 [OF u_approx])
 apply (erule finite_deflation_u_map)
 done
 
@@ -395,7 +395,7 @@
   "prj = u_map\<cdot>prj oo udom_prj u_approx"
 
 definition
-  "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
+  "defl (t::'a u itself) = u_defl\<cdot>DEFL('a)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
@@ -403,15 +403,15 @@
     using ep_pair_udom [OF u_approx]
     by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
-    unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
+  show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
+    unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map)
 qed
 
 end
 
-lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
-by (rule sfp_u_def)
+lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>DEFL('a)"
+by (rule defl_u_def)
 
 subsection {* Lifted countable types are bifinite domains *}
 
@@ -472,25 +472,25 @@
   "prj = udom_prj lift_approx"
 
 definition
-  "sfp (t::'a lift itself) =
-    (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
+  "defl (t::'a lift itself) =
+    (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
 
 instance proof
   show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
     unfolding emb_lift_def prj_lift_def
     by (rule ep_pair_udom [OF lift_approx])
-  show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
-    unfolding sfp_lift_def
+  show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
+    unfolding defl_lift_def
     apply (subst contlub_cfun_arg)
     apply (rule chainI)
-    apply (rule sfp.principal_mono)
+    apply (rule defl.principal_mono)
     apply (simp add: below_fin_defl_def)
     apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
                      ep_pair.finite_deflation_e_d_p [OF ep])
     apply (intro monofun_cfun below_refl)
     apply (rule chainE)
     apply (rule chain_lift_approx)
-    apply (subst cast_sfp_principal)
+    apply (subst cast_defl_principal)
     apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
                      ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
     done
@@ -517,14 +517,14 @@
     by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
 qed
 
-definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
+definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "ssum_defl = defl_fun2 ssum_approx ssum_map"
 
-lemma cast_ssum_sfp:
-  "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
+lemma cast_ssum_defl:
+  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
     udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
-unfolding ssum_sfp_def
-apply (rule cast_sfp_fun2 [OF ssum_approx])
+unfolding ssum_defl_def
+apply (rule cast_defl_fun2 [OF ssum_approx])
 apply (erule (1) finite_deflation_ssum_map)
 done
 
@@ -538,7 +538,7 @@
   "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
 
 definition
-  "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+  "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
@@ -546,15 +546,15 @@
     using ep_pair_udom [OF ssum_approx]
     by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
-    unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
+  show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+    unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map)
 qed
 
 end
 
-lemma SFP_ssum:
-  "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_ssum_def)
+lemma DEFL_ssum:
+  "DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_ssum_def)
 
 end
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -463,14 +463,14 @@
     by (intro finite_deflation_convex_map finite_deflation_udom_approx)
 qed
 
-definition convex_sfp :: "sfp \<rightarrow> sfp"
-where "convex_sfp = sfp_fun1 convex_approx convex_map"
+definition convex_defl :: "defl \<rightarrow> defl"
+where "convex_defl = defl_fun1 convex_approx convex_map"
 
-lemma cast_convex_sfp:
-  "cast\<cdot>(convex_sfp\<cdot>A) =
+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"
-unfolding convex_sfp_def
-apply (rule cast_sfp_fun1 [OF convex_approx])
+unfolding convex_defl_def
+apply (rule cast_defl_fun1 [OF convex_approx])
 apply (erule finite_deflation_convex_map)
 done
 
@@ -484,7 +484,7 @@
   "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
 
 definition
-  "sfp (t::'a convex_pd itself) = convex_sfp\<cdot>SFP('a)"
+  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
@@ -492,17 +492,17 @@
     using ep_pair_udom [OF convex_approx]
     by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
-    unfolding emb_convex_pd_def prj_convex_pd_def sfp_convex_pd_def cast_convex_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq convex_map_map)
+  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 expand_cfun_eq convex_map_map)
 qed
 
 end
 
-text {* SFP of type constructor = type combinator *}
+text {* DEFL of type constructor = type combinator *}
 
-lemma SFP_convex: "SFP('a convex_pd) = convex_sfp\<cdot>SFP('a)"
-by (rule sfp_convex_pd_def)
+lemma DEFL_convex: "DEFL('a convex_pd) = convex_defl\<cdot>DEFL('a)"
+by (rule defl_convex_pd_def)
 
 
 subsection {* Join *}
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Library/Strict_Fun.thy
--- a/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -162,14 +162,14 @@
     by (intro finite_deflation_sfun_map finite_deflation_udom_approx)
 qed
 
-definition sfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "sfun_sfp = sfp_fun2 sfun_approx sfun_map"
+definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+where "sfun_defl = defl_fun2 sfun_approx sfun_map"
 
-lemma cast_sfun_sfp:
-  "cast\<cdot>(sfun_sfp\<cdot>A\<cdot>B) =
+lemma cast_sfun_defl:
+  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
     udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
-unfolding sfun_sfp_def
-apply (rule cast_sfp_fun2 [OF sfun_approx])
+unfolding sfun_defl_def
+apply (rule cast_defl_fun2 [OF sfun_approx])
 apply (erule (1) finite_deflation_sfun_map)
 done
 
@@ -183,7 +183,7 @@
   "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
 
 definition
-  "sfp (t::('a \<rightarrow>! 'b) itself) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+  "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
@@ -191,29 +191,29 @@
     using ep_pair_udom [OF sfun_approx]
     by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
-    unfolding emb_sfun_def prj_sfun_def sfp_sfun_def cast_sfun_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq sfun_map_map)
+  show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
+    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
 qed
 
 end
 
-lemma SFP_sfun:
-  "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_sfun_def)
+lemma DEFL_sfun:
+  "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+by (rule defl_sfun_def)
 
 lemma isodefl_sfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_sfp\<cdot>t1\<cdot>t2)"
+    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_sfun_sfp cast_isodefl)
+apply (simp add: cast_sfun_defl cast_isodefl)
 apply (simp add: emb_sfun_def prj_sfun_def)
 apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
 done
 
 setup {*
   Domain_Isomorphism.add_type_constructor
-    (@{type_name "sfun"}, @{term sfun_sfp}, @{const_name sfun_map}, @{thm SFP_sfun},
+    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm DEFL_sfun},
        @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
 *}
 
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -452,14 +452,14 @@
     by (intro finite_deflation_lower_map finite_deflation_udom_approx)
 qed
 
-definition lower_sfp :: "sfp \<rightarrow> sfp"
-where "lower_sfp = sfp_fun1 lower_approx lower_map"
+definition lower_defl :: "defl \<rightarrow> defl"
+where "lower_defl = defl_fun1 lower_approx lower_map"
 
-lemma cast_lower_sfp:
-  "cast\<cdot>(lower_sfp\<cdot>A) =
+lemma cast_lower_defl:
+  "cast\<cdot>(lower_defl\<cdot>A) =
     udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
-unfolding lower_sfp_def
-apply (rule cast_sfp_fun1 [OF lower_approx])
+unfolding lower_defl_def
+apply (rule cast_defl_fun1 [OF lower_approx])
 apply (erule finite_deflation_lower_map)
 done
 
@@ -473,7 +473,7 @@
   "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
 
 definition
-  "sfp (t::'a lower_pd itself) = lower_sfp\<cdot>SFP('a)"
+  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
@@ -481,15 +481,15 @@
     using ep_pair_udom [OF lower_approx]
     by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
-    unfolding emb_lower_pd_def prj_lower_pd_def sfp_lower_pd_def cast_lower_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq lower_map_map)
+  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
+    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq lower_map_map)
 qed
 
 end
 
-lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
-by (rule sfp_lower_pd_def)
+lemma DEFL_lower: "DEFL('a lower_pd) = lower_defl\<cdot>DEFL('a)"
+by (rule defl_lower_pd_def)
 
 
 subsection {* Join *}
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Powerdomains.thy
--- a/src/HOLCF/Powerdomains.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Powerdomains.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -9,25 +9,25 @@
 begin
 
 lemma isodefl_upper:
-  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_sfp\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_upper_sfp cast_isodefl)
+apply (simp add: cast_upper_defl cast_isodefl)
 apply (simp add: emb_upper_pd_def prj_upper_pd_def)
 apply (simp add: upper_map_map)
 done
 
 lemma isodefl_lower:
-  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_sfp\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_lower_sfp cast_isodefl)
+apply (simp add: cast_lower_defl cast_isodefl)
 apply (simp add: emb_lower_pd_def prj_lower_pd_def)
 apply (simp add: lower_map_map)
 done
 
 lemma isodefl_convex:
-  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_sfp\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_convex_sfp cast_isodefl)
+apply (simp add: cast_convex_defl cast_isodefl)
 apply (simp add: emb_convex_pd_def prj_convex_pd_def)
 apply (simp add: convex_map_map)
 done
@@ -36,16 +36,16 @@
 
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name "upper_pd"}, @{term upper_sfp}, @{const_name upper_map},
-        @{thm SFP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
+    [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
+        @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
           @{thm deflation_upper_map}),
 
-     (@{type_name "lower_pd"}, @{term lower_sfp}, @{const_name lower_map},
-        @{thm SFP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
+     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
+        @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
           @{thm deflation_lower_map}),
 
-     (@{type_name "convex_pd"}, @{term convex_sfp}, @{const_name convex_map},
-        @{thm SFP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
+     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
+        @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
           @{thm deflation_convex_map})]
 *}
 
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Representable.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -15,20 +15,20 @@
 
 subsection {* Representations of types *}
 
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
-by (simp add: cast_SFP)
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
+by (simp add: cast_DEFL)
 
-lemma in_SFP_iff:
-  "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
-by (simp add: in_sfp_def cast_SFP)
+lemma in_DEFL_iff:
+  "x ::: DEFL('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+by (simp add: in_defl_def cast_DEFL)
 
 lemma prj_inverse:
-  "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
-by (simp only: in_SFP_iff)
+  "x ::: DEFL('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+by (simp only: in_DEFL_iff)
 
-lemma emb_in_SFP [simp]:
-  "emb\<cdot>(x::'a) ::: SFP('a)"
-by (simp add: in_SFP_iff)
+lemma emb_in_DEFL [simp]:
+  "emb\<cdot>(x::'a) ::: DEFL('a)"
+by (simp add: in_DEFL_iff)
 
 subsection {* Coerce operator *}
 
@@ -48,16 +48,16 @@
 by (rule ext_cfun, simp add: beta_coerce)
 
 lemma emb_coerce:
-  "SFP('a) \<sqsubseteq> SFP('b)
+  "DEFL('a) \<sqsubseteq> DEFL('b)
    \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
  apply (simp add: beta_coerce)
  apply (rule prj_inverse)
- apply (erule sfp_belowD)
- apply (rule emb_in_SFP)
+ apply (erule defl_belowD)
+ apply (rule emb_in_DEFL)
 done
 
 lemma coerce_prj:
-  "SFP('a) \<sqsubseteq> SFP('b)
+  "DEFL('a) \<sqsubseteq> DEFL('b)
    \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
  apply (simp add: coerce_def)
  apply (rule emb_eq_iff [THEN iffD1])
@@ -69,21 +69,21 @@
 done
 
 lemma coerce_coerce [simp]:
-  "SFP('a) \<sqsubseteq> SFP('b)
+  "DEFL('a) \<sqsubseteq> DEFL('b)
    \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
-by (simp add: beta_coerce prj_inverse sfp_belowD)
+by (simp add: beta_coerce prj_inverse defl_belowD)
 
 lemma coerce_inverse:
-  "emb\<cdot>(x::'a) ::: SFP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
+  "emb\<cdot>(x::'a) ::: DEFL('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
 by (simp only: beta_coerce prj_inverse emb_inverse)
 
 lemma coerce_type:
-  "SFP('a) \<sqsubseteq> SFP('b)
-   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: SFP('a)"
-by (simp add: beta_coerce prj_inverse sfp_belowD)
+  "DEFL('a) \<sqsubseteq> DEFL('b)
+   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: DEFL('a)"
+by (simp add: beta_coerce prj_inverse defl_belowD)
 
 lemma ep_pair_coerce:
-  "SFP('a) \<sqsubseteq> SFP('b)
+  "DEFL('a) \<sqsubseteq> DEFL('b)
    \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
  apply (rule ep_pair.intro)
   apply simp
@@ -98,19 +98,19 @@
 
 lemma domain_abs_iso:
   fixes abs and rep
-  assumes SFP: "SFP('b) = SFP('a)"
+  assumes DEFL: "DEFL('b) = DEFL('a)"
   assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   shows "rep\<cdot>(abs\<cdot>x) = x"
-unfolding abs_def rep_def by (simp add: SFP)
+unfolding abs_def rep_def by (simp add: DEFL)
 
 lemma domain_rep_iso:
   fixes abs and rep
-  assumes SFP: "SFP('b) = SFP('a)"
+  assumes DEFL: "DEFL('b) = DEFL('a)"
   assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   shows "abs\<cdot>(rep\<cdot>x) = x"
-unfolding abs_def rep_def by (simp add: SFP [symmetric])
+unfolding abs_def rep_def by (simp add: DEFL [symmetric])
 
 
 subsection {* Proving a subtype is representable *}
@@ -120,7 +120,7 @@
 *}
 
 setup {* Sign.add_const_constraint
-  (@{const_name sfp}, SOME @{typ "'a::pcpo itself \<Rightarrow> sfp"}) *}
+  (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) *}
 
 setup {* Sign.add_const_constraint
   (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
@@ -131,16 +131,16 @@
 lemma typedef_rep_class:
   fixes Rep :: "'a::pcpo \<Rightarrow> udom"
   fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
-  fixes t :: sfp
+  fixes t :: defl
   assumes type: "type_definition Rep Abs {x. x ::: t}"
   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   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)"
+  assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
   shows "OFCLASS('a, bifinite_class)"
 proof
   have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
-    by (simp add: adm_in_sfp)
+    by (simp add: adm_in_defl)
   have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
     unfolding emb
     apply (rule beta_cfun)
@@ -152,12 +152,12 @@
     apply (rule typedef_cont_Abs [OF type below adm])
     apply simp_all
     done
-  have emb_in_sfp: "\<And>x::'a. emb\<cdot>x ::: t"
+  have emb_in_defl: "\<And>x::'a. emb\<cdot>x ::: t"
     using type_definition.Rep [OF type]
     by (simp add: emb_beta)
   have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
     unfolding prj_beta
-    apply (simp add: cast_fixed [OF emb_in_sfp])
+    apply (simp add: cast_fixed [OF emb_in_defl])
     apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
     done
   have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
@@ -168,19 +168,19 @@
     apply (simp add: prj_emb)
     apply (simp add: emb_prj cast.below)
     done
-  show "cast\<cdot>SFP('a) = emb oo (prj :: udom \<rightarrow> 'a)"
-    by (rule ext_cfun, simp add: sfp emb_prj)
+  show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
+    by (rule ext_cfun, simp add: defl emb_prj)
 qed
 
-lemma typedef_SFP:
-  assumes "sfp \<equiv> (\<lambda>a::'a::pcpo itself. t)"
-  shows "SFP('a::pcpo) = t"
+lemma typedef_DEFL:
+  assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
+  shows "DEFL('a::pcpo) = t"
 unfolding assms ..
 
 text {* Restore original typing constraints *}
 
 setup {* Sign.add_const_constraint
-  (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
+  (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) *}
 
 setup {* Sign.add_const_constraint
   (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
@@ -188,15 +188,15 @@
 setup {* Sign.add_const_constraint
   (@{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)
+lemma adm_mem_Collect_in_defl: "adm (\<lambda>x. x \<in> {x. x ::: A})"
+unfolding mem_Collect_eq by (rule adm_in_defl)
 
 use "Tools/repdef.ML"
 
 subsection {* Isomorphic deflations *}
 
 definition
-  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
+  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
 where
   "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
 
@@ -222,12 +222,12 @@
     using cast.below [of t "emb\<cdot>x"] by simp
 qed
 
-lemma isodefl_ID_SFP: "isodefl (ID :: 'a \<rightarrow> 'a) SFP('a)"
-unfolding isodefl_def by (simp add: cast_SFP)
+lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
+unfolding isodefl_def by (simp add: cast_DEFL)
 
-lemma isodefl_SFP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) SFP('a) \<Longrightarrow> d = ID"
+lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
 unfolding isodefl_def
-apply (simp add: cast_SFP)
+apply (simp add: cast_DEFL)
 apply (simp add: expand_cfun_eq)
 apply (rule allI)
 apply (drule_tac x="emb\<cdot>x" in spec)
@@ -260,61 +260,61 @@
 
 lemma isodefl_coerce:
   fixes d :: "'a \<rightarrow> 'a"
-  assumes SFP: "SFP('b) = SFP('a)"
+  assumes DEFL: "DEFL('b) = DEFL('a)"
   shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
 unfolding isodefl_def
 apply (simp add: expand_cfun_eq)
-apply (simp add: emb_coerce coerce_prj SFP)
+apply (simp add: emb_coerce coerce_prj DEFL)
 done
 
 lemma isodefl_abs_rep:
   fixes abs and rep and d
-  assumes SFP: "SFP('b) = SFP('a)"
+  assumes DEFL: "DEFL('b) = DEFL('a)"
   assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
-unfolding abs_def rep_def using SFP by (rule isodefl_coerce)
+unfolding abs_def rep_def using DEFL by (rule isodefl_coerce)
 
 lemma isodefl_cfun:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_sfp\<cdot>t1\<cdot>t2)"
+    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_cfun_sfp cast_isodefl)
+apply (simp add: cast_cfun_defl cast_isodefl)
 apply (simp add: emb_cfun_def prj_cfun_def)
 apply (simp add: cfun_map_map cfcomp1)
 done
 
 lemma isodefl_ssum:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_sfp\<cdot>t1\<cdot>t2)"
+    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_ssum_sfp cast_isodefl)
+apply (simp add: cast_ssum_defl cast_isodefl)
 apply (simp add: emb_ssum_def prj_ssum_def)
 apply (simp add: ssum_map_map isodefl_strict)
 done
 
 lemma isodefl_sprod:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_sfp\<cdot>t1\<cdot>t2)"
+    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_sprod_sfp cast_isodefl)
+apply (simp add: cast_sprod_defl cast_isodefl)
 apply (simp add: emb_sprod_def prj_sprod_def)
 apply (simp add: sprod_map_map isodefl_strict)
 done
 
 lemma isodefl_cprod:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
-    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_sfp\<cdot>t1\<cdot>t2)"
+    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
-apply (simp add: cast_prod_sfp cast_isodefl)
+apply (simp add: cast_prod_defl cast_isodefl)
 apply (simp add: emb_prod_def prj_prod_def)
 apply (simp add: cprod_map_map cfcomp1)
 done
 
 lemma isodefl_u:
-  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_sfp\<cdot>t)"
+  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
 apply (rule isodeflI)
-apply (simp add: cast_u_sfp cast_isodefl)
+apply (simp add: cast_u_defl cast_isodefl)
 apply (simp add: emb_u_def prj_u_def)
 apply (simp add: u_map_map)
 done
@@ -325,19 +325,19 @@
 
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name cfun}, @{term cfun_sfp}, @{const_name cfun_map}, @{thm SFP_cfun},
+    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
         @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
 
-     (@{type_name ssum}, @{term ssum_sfp}, @{const_name ssum_map}, @{thm SFP_ssum},
+     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
         @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
 
-     (@{type_name sprod}, @{term sprod_sfp}, @{const_name sprod_map}, @{thm SFP_sprod},
+     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
         @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
 
-     (@{type_name prod}, @{term cprod_sfp}, @{const_name cprod_map}, @{thm SFP_prod},
+     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
         @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
 
-     (@{type_name "u"}, @{term u_sfp}, @{const_name u_map}, @{thm SFP_u},
+     (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
         @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
 *}
 
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Oct 11 08:32:09 2010 -0700
@@ -48,7 +48,7 @@
 
 structure DeflData = Theory_Data
 (
-  (* terms like "foo_sfp" *)
+  (* terms like "foo_defl" *)
   type T = term Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
@@ -57,7 +57,7 @@
 
 structure RepData = Theory_Data
 (
-  (* theorems like "SFP('a foo) = foo_sfp$SFP('a)" *)
+  (* theorems like "DEFL('a foo) = foo_defl$DEFL('a)" *)
   type T = thm list;
   val empty = [];
   val extend = I;
@@ -83,11 +83,11 @@
 );
 
 fun add_type_constructor
-  (tname, defl_const, map_name, SFP_thm,
+  (tname, defl_const, map_name, DEFL_thm,
    isodefl_thm, map_ID_thm, defl_map_thm) =
     DeflData.map (Symtab.insert (K true) (tname, defl_const))
     #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
-    #> RepData.map (Thm.add_thm SFP_thm)
+    #> RepData.map (Thm.add_thm DEFL_thm)
     #> IsodeflData.map (Thm.add_thm isodefl_thm)
     #> MapIdData.map (Thm.add_thm map_ID_thm);
 
@@ -104,19 +104,19 @@
 infixr 6 ->>;
 infix -->>;
 
-val sfpT = @{typ "sfp"};
+val deflT = @{typ "defl"};
 
 fun mapT (T as Type (_, Ts)) =
     (map (fn T => T ->> T) Ts) -->> (T ->> T)
   | mapT T = T ->> T;
 
-fun mk_SFP T =
-  Const (@{const_name sfp}, Term.itselfT T --> sfpT) $ Logic.mk_type T;
+fun mk_DEFL T =
+  Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
 
 fun coerce_const T = Const (@{const_name coerce}, T);
 
 fun isodefl_const T =
-  Const (@{const_name isodefl}, (T ->> T) --> sfpT --> HOLogic.boolT);
+  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
 
 fun mk_deflation t =
   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
@@ -218,13 +218,13 @@
   let
     fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
       | is_closed_typ _ = false;
-    fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, sfpT)
+    fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
       | defl_of (TVar _) = error ("defl_of_typ: TVar")
       | defl_of (T as Type (c, Ts)) =
         case Symtab.lookup tab c of
           SOME t => list_ccomb (t, map defl_of Ts)
         | NONE => if is_closed_typ T
-                  then mk_SFP T
+                  then mk_DEFL T
                   else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
   in defl_of T end;
 
@@ -443,7 +443,7 @@
     (* declare deflation combinator constants *)
     fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
       let
-        val defl_type = map (K sfpT) vs -->> sfpT;
+        val defl_type = map (K deflT) vs -->> deflT;
         val defl_bind = Binding.suffix_name "_defl" tbind;
       in
         Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
@@ -470,34 +470,34 @@
     fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
       let
         fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
-        val reps = map (mk_SFP o tfree) vs;
+        val reps = map (mk_DEFL o tfree) vs;
         val defl = list_ccomb (defl_const, reps);
-        val ((_, _, _, {SFP, ...}), thy) =
+        val ((_, _, _, {DEFL, ...}), thy) =
           Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
       in
-        (SFP, thy)
+        (DEFL, thy)
       end;
-    val (SFP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
-    val thy = RepData.map (fold Thm.add_thm SFP_thms) thy;
+    val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
+    val thy = RepData.map (fold Thm.add_thm DEFL_thms) thy;
 
-    (* prove SFP equations *)
-    fun mk_SFP_eq_thm (lhsT, rhsT) =
+    (* prove DEFL equations *)
+    fun mk_DEFL_eq_thm (lhsT, rhsT) =
       let
-        val goal = mk_eqs (mk_SFP lhsT, mk_SFP rhsT);
-        val SFP_simps = RepData.get thy;
+        val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT);
+        val DEFL_simps = RepData.get thy;
         val tac =
-          rewrite_goals_tac (map mk_meta_eq SFP_simps)
+          rewrite_goals_tac (map mk_meta_eq DEFL_simps)
           THEN resolve_tac defl_unfold_thms 1;
       in
         Goal.prove_global thy [] [] goal (K tac)
       end;
-    val SFP_eq_thms = map mk_SFP_eq_thm dom_eqns;
+    val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns;
 
-    (* register SFP equations *)
-    val SFP_eq_binds = map (Binding.prefix_name "SFP_eq_") dbinds;
+    (* register DEFL equations *)
+    val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds;
     val (_, thy) = thy |>
       (Global_Theory.add_thms o map Thm.no_attributes)
-        (SFP_eq_binds ~~ SFP_eq_thms);
+        (DEFL_eq_binds ~~ DEFL_eq_thms);
 
     (* define rep/abs functions *)
     fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
@@ -516,10 +516,10 @@
       |>> ListPair.unzip;
 
     (* prove isomorphism and isodefl rules *)
-    fun mk_iso_thms ((tbind, SFP_eq), (rep_def, abs_def)) thy =
+    fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy =
       let
         fun make thm =
-            Drule.zero_var_indexes (thm OF [SFP_eq, abs_def, rep_def]);
+            Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def]);
         val rep_iso_thm = make @{thm domain_rep_iso};
         val abs_iso_thm = make @{thm domain_abs_iso};
         val isodefl_thm = make @{thm isodefl_abs_rep};
@@ -532,7 +532,7 @@
       end;
     val ((iso_thms, isodefl_abs_rep_thms), thy) =
       thy
-      |> fold_map mk_iso_thms (dbinds ~~ SFP_eq_thms ~~ rep_abs_defs)
+      |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs)
       |>> ListPair.unzip;
 
     (* collect info about rep/abs *)
@@ -561,7 +561,7 @@
     val isodefl_thm =
       let
         fun unprime a = Library.unprefix "'" a;
-        fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), sfpT);
+        fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
         fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T);
         fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
         fun mk_goal ((map_const, defl_const), (T, rhsT)) =
@@ -579,9 +579,9 @@
           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
         val bottom_rules =
           @{thms fst_strict snd_strict isodefl_bottom simp_thms};
-        val SFP_simps = map (fn th => th RS sym) (RepData.get thy);
+        val DEFL_simps = map (fn th => th RS sym) (RepData.get thy);
         val isodefl_rules =
-          @{thms conjI isodefl_ID_SFP}
+          @{thms conjI isodefl_ID_DEFL}
           @ isodefl_abs_rep_thms
           @ IsodeflData.get thy;
       in
@@ -595,7 +595,7 @@
            simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
            simp_tac beta_ss 1,
            simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
-           simp_tac (HOL_basic_ss addsimps SFP_simps) 1,
+           simp_tac (HOL_basic_ss addsimps DEFL_simps) 1,
            REPEAT (etac @{thm conjE} 1),
            REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
       end;
@@ -613,23 +613,23 @@
 
     (* prove map_ID theorems *)
     fun prove_map_ID_thm
-        (((map_const, (lhsT, _)), SFP_thm), isodefl_thm) =
+        (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =
       let
         val Ts = snd (dest_Type lhsT);
         val lhs = list_ccomb (map_const, map mk_ID Ts);
         val goal = mk_eqs (lhs, mk_ID lhsT);
         val tac = EVERY
-          [rtac @{thm isodefl_SFP_imp_ID} 1,
-           stac SFP_thm 1,
+          [rtac @{thm isodefl_DEFL_imp_ID} 1,
+           stac DEFL_thm 1,
            rtac isodefl_thm 1,
-           REPEAT (rtac @{thm isodefl_ID_SFP} 1)];
+           REPEAT (rtac @{thm isodefl_ID_DEFL} 1)];
       in
         Goal.prove_global thy [] [] goal (K tac)
       end;
     val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds;
     val map_ID_thms =
       map prove_map_ID_thm
-        (map_consts ~~ dom_eqns ~~ SFP_thms ~~ isodefl_thms);
+        (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms);
     val (_, thy) = thy |>
       (Global_Theory.add_thms o map Thm.no_attributes)
         (map_ID_binds ~~ map_ID_thms);
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML	Mon Oct 11 08:32:09 2010 -0700
@@ -7,7 +7,7 @@
 signature REPDEF =
 sig
   type rep_info =
-    { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm }
+    { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm }
 
   val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> theory ->
@@ -28,19 +28,19 @@
 (** type definitions **)
 
 type rep_info =
-  { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm };
+  { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm };
 
 (* building types and terms *)
 
 val udomT = @{typ udom};
-val sfpT = @{typ sfp};
+val deflT = @{typ defl};
 fun emb_const T = Const (@{const_name emb}, T ->> udomT);
 fun prj_const T = Const (@{const_name prj}, udomT ->> T);
-fun sfp_const T = Const (@{const_name sfp}, Term.itselfT T --> sfpT);
+fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT);
 
 fun mk_cast (t, x) =
   capply_const (udomT, udomT)
-  $ (capply_const (sfpT, udomT ->> udomT) $ @{const cast} $ t)
+  $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
   $ x;
 
 (* manipulating theorems *)
@@ -70,8 +70,8 @@
     val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
 
     val deflT = Term.fastype_of defl;
-    val _ = if deflT = @{typ "sfp"} then ()
-            else error ("Not type sfp: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
+    val _ = if deflT = @{typ "defl"} then ()
+            else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
 
     (*lhs*)
     val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
@@ -84,12 +84,12 @@
       |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
 
     (*set*)
-    val in_defl = @{term "in_sfp :: udom => sfp => bool"};
+    val in_defl = @{term "in_defl :: udom => defl => bool"};
     val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl);
 
     (*pcpodef*)
-    val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_sfp} 1;
-    val tac2 = rtac @{thm adm_mem_Collect_in_sfp} 1;
+    val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_defl} 1;
+    val tac2 = rtac @{thm adm_mem_Collect_in_defl} 1;
     val ((info, cpo_info, pcpo_info), thy) = thy
       |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
 
@@ -99,12 +99,12 @@
     val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
     val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
       Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
-    val sfp_eqn = Logic.mk_equals (sfp_const newT,
+    val defl_eqn = Logic.mk_equals (defl_const newT,
       Abs ("x", Term.itselfT newT, defl));
     val name_def = Binding.suffix_name "_def" name;
     val emb_bind = (Binding.prefix_name "emb_" name_def, []);
     val prj_bind = (Binding.prefix_name "prj_" name_def, []);
-    val sfp_bind = (Binding.prefix_name "sfp_" name_def, []);
+    val defl_bind = (Binding.prefix_name "defl_" name_def, []);
 
     (*instantiate class rep*)
     val lthy = thy
@@ -113,34 +113,34 @@
         Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
     val ((_, (_, prj_ldef)), lthy) =
         Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
-    val ((_, (_, sfp_ldef)), lthy) =
-        Specification.definition (NONE, (sfp_bind, sfp_eqn)) lthy;
+    val ((_, (_, defl_ldef)), lthy) =
+        Specification.definition (NONE, (defl_bind, defl_eqn)) lthy;
     val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
     val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
     val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
-    val sfp_def = singleton (ProofContext.export lthy ctxt_thy) sfp_ldef;
+    val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef;
     val type_definition_thm =
       MetaSimplifier.rewrite_rule
         (the_list (#set_def (#2 info)))
         (#type_definition (#2 info));
     val typedef_thms =
-      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, sfp_def];
+      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def];
     val thy = lthy
       |> Class.prove_instantiation_instance
           (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
       |> Local_Theory.exit_global;
 
     (*other theorems*)
-    val sfp_thm' = Thm.transfer thy sfp_def;
-    val (SFP_thm, thy) = thy
+    val defl_thm' = Thm.transfer thy defl_def;
+    val (DEFL_thm, thy) = thy
       |> Sign.add_path (Binding.name_of name)
       |> Global_Theory.add_thm
-         ((Binding.prefix_name "SFP_" name,
-          Drule.zero_var_indexes (@{thm typedef_SFP} OF [sfp_thm'])), [])
+         ((Binding.prefix_name "DEFL_" name,
+          Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
       ||> Sign.restore_naming thy;
 
     val rep_info =
-      { emb_def = emb_def, prj_def = prj_def, sfp_def = sfp_def, SFP = SFP_thm };
+      { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, DEFL = DEFL_thm };
   in
     ((info, cpo_info, pcpo_info, rep_info), thy)
   end
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -447,14 +447,14 @@
     by (intro finite_deflation_upper_map finite_deflation_udom_approx)
 qed
 
-definition upper_sfp :: "sfp \<rightarrow> sfp"
-where "upper_sfp = sfp_fun1 upper_approx upper_map"
+definition upper_defl :: "defl \<rightarrow> defl"
+where "upper_defl = defl_fun1 upper_approx upper_map"
 
-lemma cast_upper_sfp:
-  "cast\<cdot>(upper_sfp\<cdot>A) =
+lemma cast_upper_defl:
+  "cast\<cdot>(upper_defl\<cdot>A) =
     udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
-unfolding upper_sfp_def
-apply (rule cast_sfp_fun1 [OF upper_approx])
+unfolding upper_defl_def
+apply (rule cast_defl_fun1 [OF upper_approx])
 apply (erule finite_deflation_upper_map)
 done
 
@@ -468,7 +468,7 @@
   "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
 
 definition
-  "sfp (t::'a upper_pd itself) = upper_sfp\<cdot>SFP('a)"
+  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
@@ -476,15 +476,15 @@
     using ep_pair_udom [OF upper_approx]
     by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
 next
-  show "cast\<cdot>SFP('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
-    unfolding emb_upper_pd_def prj_upper_pd_def sfp_upper_pd_def cast_upper_sfp
-    by (simp add: cast_SFP oo_def expand_cfun_eq upper_map_map)
+  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
+    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
+    by (simp add: cast_DEFL oo_def expand_cfun_eq upper_map_map)
 qed
 
 end
 
-lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
-by (rule sfp_upper_pd_def)
+lemma DEFL_upper: "DEFL('a upper_pd) = upper_defl\<cdot>DEFL('a)"
+by (rule defl_upper_pd_def)
 
 
 subsection {* Join *}
diff -r a4b2971952f4 -r ad60d7311f43 src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Mon Oct 11 07:09:42 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Mon Oct 11 08:32:09 2010 -0700
@@ -28,50 +28,50 @@
 text {* Start with the one-step non-recursive version *}
 
 definition
-  foo_bar_baz_sfpF ::
-    "sfp \<rightarrow> sfp \<times> sfp \<times> sfp \<rightarrow> sfp \<times> sfp \<times> sfp"
+  foo_bar_baz_deflF ::
+    "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
 where
-  "foo_bar_baz_sfpF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
-    ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>t2))
-    , u_sfp\<cdot>(cfun_sfp\<cdot>t3\<cdot>SFP(tr))
-    , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>t1)\<cdot>SFP(tr)))))"
+  "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
+    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
+    , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
+    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
 
-lemma foo_bar_baz_sfpF_beta:
-  "foo_bar_baz_sfpF\<cdot>a\<cdot>t =
-    ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(fst (snd t))))
-    , u_sfp\<cdot>(cfun_sfp\<cdot>(snd (snd t))\<cdot>SFP(tr))
-    , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(fst t))\<cdot>SFP(tr)))"
-unfolding foo_bar_baz_sfpF_def
+lemma foo_bar_baz_deflF_beta:
+  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
+    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
+    , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
+    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
+unfolding foo_bar_baz_deflF_def
 by (simp add: split_def)
 
 text {* Individual type combinators are projected from the fixed point. *}
 
-definition foo_sfp :: "sfp \<rightarrow> sfp"
-where "foo_sfp = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
+definition foo_defl :: "defl \<rightarrow> defl"
+where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
 
-definition bar_sfp :: "sfp \<rightarrow> sfp"
-where "bar_sfp = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
+definition bar_defl :: "defl \<rightarrow> defl"
+where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
-definition baz_sfp :: "sfp \<rightarrow> sfp"
-where "baz_sfp = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
+definition baz_defl :: "defl \<rightarrow> defl"
+where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
 lemma defl_apply_thms:
-  "foo_sfp\<cdot>a = fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))"
-  "bar_sfp\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
-  "baz_sfp\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
-unfolding foo_sfp_def bar_sfp_def baz_sfp_def by simp_all
+  "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
+  "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
+  "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
+unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
 
 text {* Unfold rules for each combinator. *}
 
-lemma foo_sfp_unfold:
-  "foo_sfp\<cdot>a = ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(bar_sfp\<cdot>a)))"
-unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
+lemma foo_defl_unfold:
+  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma bar_sfp_unfold: "bar_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(baz_sfp\<cdot>a)\<cdot>SFP(tr))"
-unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
+lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
-lemma baz_sfp_unfold: "baz_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(foo_sfp\<cdot>a))\<cdot>SFP(tr))"
-unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
+lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>DEFL(tr))"
+unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
 
 text "The automation for the previous steps will be quite similar to
 how the fixrec package works."
@@ -82,14 +82,14 @@
 
 text {* Use @{text pcpodef} with the appropriate type combinator. *}
 
-pcpodef (open) 'a foo = "{x. x ::: foo_sfp\<cdot>SFP('a)}"
-by (simp_all add: adm_in_sfp)
+pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>DEFL('a)}"
+by (simp_all add: adm_in_defl)
 
-pcpodef (open) 'a bar = "{x. x ::: bar_sfp\<cdot>SFP('a)}"
-by (simp_all add: adm_in_sfp)
+pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>DEFL('a)}"
+by (simp_all add: adm_in_defl)
 
-pcpodef (open) 'a baz = "{x. x ::: baz_sfp\<cdot>SFP('a)}"
-by (simp_all add: adm_in_sfp)
+pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>DEFL('a)}"
+by (simp_all add: adm_in_defl)
 
 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
 
@@ -100,10 +100,10 @@
 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
 
 definition prj_foo :: "udom \<rightarrow> 'a foo"
-where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_sfp\<cdot>SFP('a))\<cdot>y))"
+where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
 
-definition sfp_foo :: "'a foo itself \<Rightarrow> sfp"
-where "sfp_foo \<equiv> \<lambda>a. foo_sfp\<cdot>SFP('a)"
+definition defl_foo :: "'a foo itself \<Rightarrow> defl"
+where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
 
 instance
 apply (rule typedef_rep_class)
@@ -111,7 +111,7 @@
 apply (rule below_foo_def)
 apply (rule emb_foo_def)
 apply (rule prj_foo_def)
-apply (rule sfp_foo_def)
+apply (rule defl_foo_def)
 done
 
 end
@@ -123,10 +123,10 @@
 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
 
 definition prj_bar :: "udom \<rightarrow> 'a bar"
-where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_sfp\<cdot>SFP('a))\<cdot>y))"
+where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
 
-definition sfp_bar :: "'a bar itself \<Rightarrow> sfp"
-where "sfp_bar \<equiv> \<lambda>a. bar_sfp\<cdot>SFP('a)"
+definition defl_bar :: "'a bar itself \<Rightarrow> defl"
+where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
 
 instance
 apply (rule typedef_rep_class)
@@ -134,7 +134,7 @@
 apply (rule below_bar_def)
 apply (rule emb_bar_def)
 apply (rule prj_bar_def)
-apply (rule sfp_bar_def)
+apply (rule defl_bar_def)
 done
 
 end
@@ -146,10 +146,10 @@
 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
 
 definition prj_baz :: "udom \<rightarrow> 'a baz"
-where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_sfp\<cdot>SFP('a))\<cdot>y))"
+where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
 
-definition sfp_baz :: "'a baz itself \<Rightarrow> sfp"
-where "sfp_baz \<equiv> \<lambda>a. baz_sfp\<cdot>SFP('a)"
+definition defl_baz :: "'a baz itself \<Rightarrow> defl"
+where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
 
 instance
 apply (rule typedef_rep_class)
@@ -157,44 +157,44 @@
 apply (rule below_baz_def)
 apply (rule emb_baz_def)
 apply (rule prj_baz_def)
-apply (rule sfp_baz_def)
+apply (rule defl_baz_def)
 done
 
 end
 
-text {* Prove SFP rules using lemma @{text typedef_SFP}. *}
+text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
 
-lemma SFP_foo: "SFP('a foo) = foo_sfp\<cdot>SFP('a)"
-apply (rule typedef_SFP)
-apply (rule sfp_foo_def)
+lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
+apply (rule typedef_DEFL)
+apply (rule defl_foo_def)
 done
 
-lemma SFP_bar: "SFP('a bar) = bar_sfp\<cdot>SFP('a)"
-apply (rule typedef_SFP)
-apply (rule sfp_bar_def)
+lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
+apply (rule typedef_DEFL)
+apply (rule defl_bar_def)
 done
 
-lemma SFP_baz: "SFP('a baz) = baz_sfp\<cdot>SFP('a)"
-apply (rule typedef_SFP)
-apply (rule sfp_baz_def)
+lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
+apply (rule typedef_DEFL)
+apply (rule defl_baz_def)
 done
 
-text {* Prove SFP equations using type combinator unfold lemmas. *}
+text {* Prove DEFL equations using type combinator unfold lemmas. *}
 
-lemmas SFP_simps =
-  SFP_ssum SFP_sprod SFP_u SFP_cfun
+lemmas DEFL_simps =
+  DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun
 
-lemma SFP_foo': "SFP('a foo) = SFP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
-unfolding SFP_foo SFP_bar SFP_baz SFP_simps
-by (rule foo_sfp_unfold)
+lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
+unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+by (rule foo_defl_unfold)
 
-lemma SFP_bar': "SFP('a bar) = SFP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding SFP_foo SFP_bar SFP_baz SFP_simps
-by (rule bar_sfp_unfold)
+lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
+unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
+by (rule bar_defl_unfold)
 
-lemma SFP_baz': "SFP('a baz) = SFP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding SFP_foo SFP_bar SFP_baz SFP_simps SFP_convex
-by (rule baz_sfp_unfold)
+lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
+unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps DEFL_convex
+by (rule baz_defl_unfold)
 
 (********************************************************************)
 
@@ -223,36 +223,36 @@
 text {* Prove isomorphism rules. *}
 
 lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
-by (rule domain_abs_iso [OF SFP_foo' foo_abs_def foo_rep_def])
+by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
 
 lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
-by (rule domain_rep_iso [OF SFP_foo' foo_abs_def foo_rep_def])
+by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
 
 lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
-by (rule domain_abs_iso [OF SFP_bar' bar_abs_def bar_rep_def])
+by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
 
 lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
-by (rule domain_rep_iso [OF SFP_bar' bar_abs_def bar_rep_def])
+by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
 
 lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
-by (rule domain_abs_iso [OF SFP_baz' baz_abs_def baz_rep_def])
+by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
 
 lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
-by (rule domain_rep_iso [OF SFP_baz' baz_abs_def baz_rep_def])
+by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
 
 text {* Prove isodefl rules using @{text isodefl_coerce}. *}
 
 lemma isodefl_foo_abs:
   "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
-by (rule isodefl_abs_rep [OF SFP_foo' foo_abs_def foo_rep_def])
+by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
 
 lemma isodefl_bar_abs:
   "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
-by (rule isodefl_abs_rep [OF SFP_bar' bar_abs_def bar_rep_def])
+by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
 
 lemma isodefl_baz_abs:
   "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
-by (rule isodefl_abs_rep [OF SFP_baz' baz_abs_def baz_rep_def])
+by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
 
 (********************************************************************)
 
@@ -316,15 +316,15 @@
 lemma isodefl_foo_bar_baz:
   assumes isodefl_d: "isodefl d t"
   shows
-  "isodefl (foo_map\<cdot>d) (foo_sfp\<cdot>t) \<and>
-  isodefl (bar_map\<cdot>d) (bar_sfp\<cdot>t) \<and>
-  isodefl (baz_map\<cdot>d) (baz_sfp\<cdot>t)"
+  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
+  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
+  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
 unfolding map_apply_thms defl_apply_thms
  apply (rule parallel_fix_ind)
    apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
   apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
  apply (simp only: foo_bar_baz_mapF_beta
-                   foo_bar_baz_sfpF_beta
+                   foo_bar_baz_deflF_beta
                    fst_conv snd_conv)
  apply (elim conjE)
  apply (intro
@@ -332,7 +332,7 @@
   isodefl_foo_abs
   isodefl_bar_abs
   isodefl_baz_abs
-  isodefl_ssum isodefl_sprod isodefl_ID_SFP
+  isodefl_ssum isodefl_sprod isodefl_ID_DEFL
   isodefl_u isodefl_convex isodefl_cfun
   isodefl_d
  )
@@ -343,27 +343,27 @@
 lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
 lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
 
-text {* Prove map ID lemmas, using isodefl_SFP_imp_ID *}
+text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
 
 lemma foo_map_ID: "foo_map\<cdot>ID = ID"
-apply (rule isodefl_SFP_imp_ID)
-apply (subst SFP_foo)
+apply (rule isodefl_DEFL_imp_ID)
+apply (subst DEFL_foo)
 apply (rule isodefl_foo)
-apply (rule isodefl_ID_SFP)
+apply (rule isodefl_ID_DEFL)
 done
 
 lemma bar_map_ID: "bar_map\<cdot>ID = ID"
-apply (rule isodefl_SFP_imp_ID)
-apply (subst SFP_bar)
+apply (rule isodefl_DEFL_imp_ID)
+apply (subst DEFL_bar)
 apply (rule isodefl_bar)
-apply (rule isodefl_ID_SFP)
+apply (rule isodefl_ID_DEFL)
 done
 
 lemma baz_map_ID: "baz_map\<cdot>ID = ID"
-apply (rule isodefl_SFP_imp_ID)
-apply (subst SFP_baz)
+apply (rule isodefl_DEFL_imp_ID)
+apply (subst DEFL_baz)
 apply (rule isodefl_baz)
-apply (rule isodefl_ID_SFP)
+apply (rule isodefl_ID_DEFL)
 done
 
 (********************************************************************)