renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
authorhuffman
Mon Oct 11 08:32:09 2010 -0700 (2010-10-11)
changeset 39989ad60d7311f43
parent 39988 a4b2971952f4
child 39990 9b4341366b63
child 39999 e3948547b541
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
src/HOLCF/Algebraic.thy
src/HOLCF/Bifinite.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Library/Strict_Fun.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Powerdomains.thy
src/HOLCF/Representable.thy
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/repdef.ML
src/HOLCF/UpperPD.thy
src/HOLCF/ex/Domain_Proofs.thy
     1.1 --- a/src/HOLCF/Algebraic.thy	Mon Oct 11 07:09:42 2010 -0700
     1.2 +++ b/src/HOLCF/Algebraic.thy	Mon Oct 11 08:32:09 2010 -0700
     1.3 @@ -72,36 +72,29 @@
     1.4  
     1.5  subsection {* Defining algebraic deflations by ideal completion *}
     1.6  
     1.7 -text {*
     1.8 -  An SFP domain is one that can be represented as the limit of a
     1.9 -  sequence of finite posets.  Here we use omega-algebraic deflations
    1.10 -  (i.e. countable ideals of finite deflations) to model sequences of
    1.11 -  finite posets.
    1.12 -*}
    1.13 -
    1.14 -typedef (open) sfp = "{S::fin_defl set. below.ideal S}"
    1.15 +typedef (open) defl = "{S::fin_defl set. below.ideal S}"
    1.16  by (fast intro: below.ideal_principal)
    1.17  
    1.18 -instantiation sfp :: below
    1.19 +instantiation defl :: below
    1.20  begin
    1.21  
    1.22  definition
    1.23 -  "x \<sqsubseteq> y \<longleftrightarrow> Rep_sfp x \<subseteq> Rep_sfp y"
    1.24 +  "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
    1.25  
    1.26  instance ..
    1.27  end
    1.28  
    1.29 -instance sfp :: po
    1.30 -using type_definition_sfp below_sfp_def
    1.31 +instance defl :: po
    1.32 +using type_definition_defl below_defl_def
    1.33  by (rule below.typedef_ideal_po)
    1.34  
    1.35 -instance sfp :: cpo
    1.36 -using type_definition_sfp below_sfp_def
    1.37 +instance defl :: cpo
    1.38 +using type_definition_defl below_defl_def
    1.39  by (rule below.typedef_ideal_cpo)
    1.40  
    1.41  definition
    1.42 -  sfp_principal :: "fin_defl \<Rightarrow> sfp" where
    1.43 -  "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
    1.44 +  defl_principal :: "fin_defl \<Rightarrow> defl" where
    1.45 +  "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
    1.46  
    1.47  lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
    1.48  proof
    1.49 @@ -130,52 +123,52 @@
    1.50      done
    1.51  qed
    1.52  
    1.53 -interpretation sfp: ideal_completion below sfp_principal Rep_sfp
    1.54 -using type_definition_sfp below_sfp_def
    1.55 -using sfp_principal_def fin_defl_countable
    1.56 +interpretation defl: ideal_completion below defl_principal Rep_defl
    1.57 +using type_definition_defl below_defl_def
    1.58 +using defl_principal_def fin_defl_countable
    1.59  by (rule below.typedef_ideal_completion)
    1.60  
    1.61  text {* Algebraic deflations are pointed *}
    1.62  
    1.63 -lemma sfp_minimal: "sfp_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
    1.64 -apply (induct x rule: sfp.principal_induct, simp)
    1.65 -apply (rule sfp.principal_mono)
    1.66 +lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
    1.67 +apply (induct x rule: defl.principal_induct, simp)
    1.68 +apply (rule defl.principal_mono)
    1.69  apply (simp add: below_fin_defl_def)
    1.70  apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
    1.71  done
    1.72  
    1.73 -instance sfp :: pcpo
    1.74 -by intro_classes (fast intro: sfp_minimal)
    1.75 +instance defl :: pcpo
    1.76 +by intro_classes (fast intro: defl_minimal)
    1.77  
    1.78 -lemma inst_sfp_pcpo: "\<bottom> = sfp_principal (Abs_fin_defl \<bottom>)"
    1.79 -by (rule sfp_minimal [THEN UU_I, symmetric])
    1.80 +lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
    1.81 +by (rule defl_minimal [THEN UU_I, symmetric])
    1.82  
    1.83  subsection {* Applying algebraic deflations *}
    1.84  
    1.85  definition
    1.86 -  cast :: "sfp \<rightarrow> udom \<rightarrow> udom"
    1.87 +  cast :: "defl \<rightarrow> udom \<rightarrow> udom"
    1.88  where
    1.89 -  "cast = sfp.basis_fun Rep_fin_defl"
    1.90 +  "cast = defl.basis_fun Rep_fin_defl"
    1.91  
    1.92 -lemma cast_sfp_principal:
    1.93 -  "cast\<cdot>(sfp_principal a) = Rep_fin_defl a"
    1.94 +lemma cast_defl_principal:
    1.95 +  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
    1.96  unfolding cast_def
    1.97 -apply (rule sfp.basis_fun_principal)
    1.98 +apply (rule defl.basis_fun_principal)
    1.99  apply (simp only: below_fin_defl_def)
   1.100  done
   1.101  
   1.102  lemma deflation_cast: "deflation (cast\<cdot>d)"
   1.103 -apply (induct d rule: sfp.principal_induct)
   1.104 +apply (induct d rule: defl.principal_induct)
   1.105  apply (rule adm_subst [OF _ adm_deflation], simp)
   1.106 -apply (simp add: cast_sfp_principal)
   1.107 +apply (simp add: cast_defl_principal)
   1.108  apply (rule finite_deflation_imp_deflation)
   1.109  apply (rule finite_deflation_Rep_fin_defl)
   1.110  done
   1.111  
   1.112  lemma finite_deflation_cast:
   1.113    "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
   1.114 -apply (drule sfp.compact_imp_principal, clarify)
   1.115 -apply (simp add: cast_sfp_principal)
   1.116 +apply (drule defl.compact_imp_principal, clarify)
   1.117 +apply (simp add: cast_defl_principal)
   1.118  apply (rule finite_deflation_Rep_fin_defl)
   1.119  done
   1.120  
   1.121 @@ -190,9 +183,9 @@
   1.122  done
   1.123  
   1.124  lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
   1.125 -apply (induct A rule: sfp.principal_induct, simp)
   1.126 -apply (induct B rule: sfp.principal_induct, simp)
   1.127 -apply (simp add: cast_sfp_principal below_fin_defl_def)
   1.128 +apply (induct A rule: defl.principal_induct, simp)
   1.129 +apply (induct B rule: defl.principal_induct, simp)
   1.130 +apply (simp add: cast_defl_principal below_fin_defl_def)
   1.131  done
   1.132  
   1.133  lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
   1.134 @@ -209,8 +202,8 @@
   1.135  by (simp add: below_antisym cast_below_imp_below)
   1.136  
   1.137  lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
   1.138 -apply (subst inst_sfp_pcpo)
   1.139 -apply (subst cast_sfp_principal)
   1.140 +apply (subst inst_defl_pcpo)
   1.141 +apply (subst cast_defl_principal)
   1.142  apply (rule Abs_fin_defl_inverse)
   1.143  apply (simp add: finite_deflation_UU)
   1.144  done
   1.145 @@ -221,40 +214,40 @@
   1.146  subsection {* Deflation membership relation *}
   1.147  
   1.148  definition
   1.149 -  in_sfp :: "udom \<Rightarrow> sfp \<Rightarrow> bool" (infixl ":::" 50)
   1.150 +  in_defl :: "udom \<Rightarrow> defl \<Rightarrow> bool" (infixl ":::" 50)
   1.151  where
   1.152    "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
   1.153  
   1.154 -lemma adm_in_sfp: "adm (\<lambda>x. x ::: A)"
   1.155 -unfolding in_sfp_def by simp
   1.156 +lemma adm_in_defl: "adm (\<lambda>x. x ::: A)"
   1.157 +unfolding in_defl_def by simp
   1.158  
   1.159 -lemma in_sfpI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
   1.160 -unfolding in_sfp_def .
   1.161 +lemma in_deflI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
   1.162 +unfolding in_defl_def .
   1.163  
   1.164  lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
   1.165 -unfolding in_sfp_def .
   1.166 +unfolding in_defl_def .
   1.167  
   1.168 -lemma cast_in_sfp [simp]: "cast\<cdot>A\<cdot>x ::: A"
   1.169 -unfolding in_sfp_def by (rule cast.idem)
   1.170 +lemma cast_in_defl [simp]: "cast\<cdot>A\<cdot>x ::: A"
   1.171 +unfolding in_defl_def by (rule cast.idem)
   1.172  
   1.173 -lemma bottom_in_sfp [simp]: "\<bottom> ::: A"
   1.174 -unfolding in_sfp_def by (rule cast_strict2)
   1.175 +lemma bottom_in_defl [simp]: "\<bottom> ::: A"
   1.176 +unfolding in_defl_def by (rule cast_strict2)
   1.177  
   1.178 -lemma sfp_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
   1.179 -unfolding in_sfp_def
   1.180 +lemma defl_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
   1.181 +unfolding in_defl_def
   1.182   apply (rule deflation.belowD)
   1.183     apply (rule deflation_cast)
   1.184    apply (erule monofun_cfun_arg)
   1.185   apply assumption
   1.186  done
   1.187  
   1.188 -lemma rev_sfp_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
   1.189 -by (rule sfp_belowD)
   1.190 +lemma rev_defl_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
   1.191 +by (rule defl_belowD)
   1.192  
   1.193 -lemma sfp_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
   1.194 +lemma defl_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
   1.195  apply (rule cast_below_imp_below)
   1.196  apply (rule cast.belowI)
   1.197 -apply (simp add: in_sfp_def)
   1.198 +apply (simp add: in_defl_def)
   1.199  done
   1.200  
   1.201  end
     2.1 --- a/src/HOLCF/Bifinite.thy	Mon Oct 11 07:09:42 2010 -0700
     2.2 +++ b/src/HOLCF/Bifinite.thy	Mon Oct 11 08:32:09 2010 -0700
     2.3 @@ -18,12 +18,12 @@
     2.4  class bifinite = pcpo +
     2.5    fixes emb :: "'a::pcpo \<rightarrow> udom"
     2.6    fixes prj :: "udom \<rightarrow> 'a::pcpo"
     2.7 -  fixes sfp :: "'a itself \<Rightarrow> sfp"
     2.8 +  fixes defl :: "'a itself \<Rightarrow> defl"
     2.9    assumes ep_pair_emb_prj: "ep_pair emb prj"
    2.10 -  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
    2.11 +  assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
    2.12  
    2.13 -syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
    2.14 -translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
    2.15 +syntax "_DEFL" :: "type \<Rightarrow> defl"  ("(1DEFL/(1'(_')))")
    2.16 +translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
    2.17  
    2.18  interpretation bifinite:
    2.19    pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
    2.20 @@ -47,24 +47,24 @@
    2.21    ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
    2.22  proof -
    2.23    obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
    2.24 -  and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
    2.25 -    by (rule sfp.obtain_principal_chain)
    2.26 -  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
    2.27 -  interpret sfp_approx: approx_chain approx
    2.28 +  and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
    2.29 +    by (rule defl.obtain_principal_chain)
    2.30 +  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
    2.31 +  interpret defl_approx: approx_chain approx
    2.32    proof (rule approx_chain.intro)
    2.33      show "chain (\<lambda>i. approx i)"
    2.34        unfolding approx_def by (simp add: Y)
    2.35      show "(\<Squnion>i. approx i) = ID"
    2.36        unfolding approx_def
    2.37 -      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
    2.38 +      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq)
    2.39      show "\<And>i. finite_deflation (approx i)"
    2.40        unfolding approx_def
    2.41        apply (rule bifinite.finite_deflation_p_d_e)
    2.42        apply (rule finite_deflation_cast)
    2.43 -      apply (rule sfp.compact_principal)
    2.44 +      apply (rule defl.compact_principal)
    2.45        apply (rule below_trans [OF monofun_cfun_fun])
    2.46        apply (rule is_ub_thelub, simp add: Y)
    2.47 -      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
    2.48 +      apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL)
    2.49        done
    2.50    qed
    2.51    (* FIXME: why does show ?thesis fail here? *)
    2.52 @@ -74,30 +74,30 @@
    2.53  subsection {* Type combinators *}
    2.54  
    2.55  definition
    2.56 -  sfp_fun1 ::
    2.57 -    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
    2.58 +  defl_fun1 ::
    2.59 +    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
    2.60  where
    2.61 -  "sfp_fun1 approx f =
    2.62 -    sfp.basis_fun (\<lambda>a.
    2.63 -      sfp_principal (Abs_fin_defl
    2.64 +  "defl_fun1 approx f =
    2.65 +    defl.basis_fun (\<lambda>a.
    2.66 +      defl_principal (Abs_fin_defl
    2.67          (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
    2.68  
    2.69  definition
    2.70 -  sfp_fun2 ::
    2.71 +  defl_fun2 ::
    2.72      "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
    2.73 -      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
    2.74 +      \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)"
    2.75  where
    2.76 -  "sfp_fun2 approx f =
    2.77 -    sfp.basis_fun (\<lambda>a.
    2.78 -      sfp.basis_fun (\<lambda>b.
    2.79 -        sfp_principal (Abs_fin_defl
    2.80 +  "defl_fun2 approx f =
    2.81 +    defl.basis_fun (\<lambda>a.
    2.82 +      defl.basis_fun (\<lambda>b.
    2.83 +        defl_principal (Abs_fin_defl
    2.84            (udom_emb approx oo
    2.85              f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
    2.86  
    2.87 -lemma cast_sfp_fun1:
    2.88 +lemma cast_defl_fun1:
    2.89    assumes approx: "approx_chain approx"
    2.90    assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
    2.91 -  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
    2.92 +  shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
    2.93  proof -
    2.94    have 1: "\<And>a. finite_deflation
    2.95          (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
    2.96 @@ -106,23 +106,23 @@
    2.97      apply (rule f, rule finite_deflation_Rep_fin_defl)
    2.98      done
    2.99    show ?thesis
   2.100 -    by (induct A rule: sfp.principal_induct, simp)
   2.101 -       (simp only: sfp_fun1_def
   2.102 -                   sfp.basis_fun_principal
   2.103 -                   sfp.basis_fun_mono
   2.104 -                   sfp.principal_mono
   2.105 +    by (induct A rule: defl.principal_induct, simp)
   2.106 +       (simp only: defl_fun1_def
   2.107 +                   defl.basis_fun_principal
   2.108 +                   defl.basis_fun_mono
   2.109 +                   defl.principal_mono
   2.110                     Abs_fin_defl_mono [OF 1 1]
   2.111                     monofun_cfun below_refl
   2.112                     Rep_fin_defl_mono
   2.113 -                   cast_sfp_principal
   2.114 +                   cast_defl_principal
   2.115                     Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   2.116  qed
   2.117  
   2.118 -lemma cast_sfp_fun2:
   2.119 +lemma cast_defl_fun2:
   2.120    assumes approx: "approx_chain approx"
   2.121    assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
   2.122                  finite_deflation (f\<cdot>a\<cdot>b)"
   2.123 -  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
   2.124 +  shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) =
   2.125      udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
   2.126  proof -
   2.127    have 1: "\<And>a b. finite_deflation (udom_emb approx oo
   2.128 @@ -132,15 +132,15 @@
   2.129      apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
   2.130      done
   2.131    show ?thesis
   2.132 -    by (induct A B rule: sfp.principal_induct2, simp, simp)
   2.133 -       (simp only: sfp_fun2_def
   2.134 -                   sfp.basis_fun_principal
   2.135 -                   sfp.basis_fun_mono
   2.136 -                   sfp.principal_mono
   2.137 +    by (induct A B rule: defl.principal_induct2, simp, simp)
   2.138 +       (simp only: defl_fun2_def
   2.139 +                   defl.basis_fun_principal
   2.140 +                   defl.basis_fun_mono
   2.141 +                   defl.principal_mono
   2.142                     Abs_fin_defl_mono [OF 1 1]
   2.143                     monofun_cfun below_refl
   2.144                     Rep_fin_defl_mono
   2.145 -                   cast_sfp_principal
   2.146 +                   cast_defl_principal
   2.147                     Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   2.148  qed
   2.149  
   2.150 @@ -156,22 +156,22 @@
   2.151    "prj = (ID :: udom \<rightarrow> udom)"
   2.152  
   2.153  definition
   2.154 -  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
   2.155 +  "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
   2.156  
   2.157  instance proof
   2.158    show "ep_pair emb (prj :: udom \<rightarrow> udom)"
   2.159      by (simp add: ep_pair.intro)
   2.160  next
   2.161 -  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
   2.162 -    unfolding sfp_udom_def
   2.163 +  show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
   2.164 +    unfolding defl_udom_def
   2.165      apply (subst contlub_cfun_arg)
   2.166      apply (rule chainI)
   2.167 -    apply (rule sfp.principal_mono)
   2.168 +    apply (rule defl.principal_mono)
   2.169      apply (simp add: below_fin_defl_def)
   2.170      apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
   2.171      apply (rule chainE)
   2.172      apply (rule chain_udom_approx)
   2.173 -    apply (subst cast_sfp_principal)
   2.174 +    apply (subst cast_defl_principal)
   2.175      apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
   2.176      done
   2.177  qed
   2.178 @@ -197,14 +197,14 @@
   2.179      by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
   2.180  qed
   2.181  
   2.182 -definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   2.183 -where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
   2.184 +definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   2.185 +where "cfun_defl = defl_fun2 cfun_approx cfun_map"
   2.186  
   2.187 -lemma cast_cfun_sfp:
   2.188 -  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
   2.189 +lemma cast_cfun_defl:
   2.190 +  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
   2.191      udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
   2.192 -unfolding cfun_sfp_def
   2.193 -apply (rule cast_sfp_fun2 [OF cfun_approx])
   2.194 +unfolding cfun_defl_def
   2.195 +apply (rule cast_defl_fun2 [OF cfun_approx])
   2.196  apply (erule (1) finite_deflation_cfun_map)
   2.197  done
   2.198  
   2.199 @@ -218,7 +218,7 @@
   2.200    "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
   2.201  
   2.202  definition
   2.203 -  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.204 +  "defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.205  
   2.206  instance proof
   2.207    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   2.208 @@ -226,16 +226,16 @@
   2.209      using ep_pair_udom [OF cfun_approx]
   2.210      by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
   2.211  next
   2.212 -  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   2.213 -    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
   2.214 -    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
   2.215 +  show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   2.216 +    unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
   2.217 +    by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map)
   2.218  qed
   2.219  
   2.220  end
   2.221  
   2.222 -lemma SFP_cfun:
   2.223 -  "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.224 -by (rule sfp_cfun_def)
   2.225 +lemma DEFL_cfun:
   2.226 +  "DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.227 +by (rule defl_cfun_def)
   2.228  
   2.229  subsection {* Cartesian product is a bifinite domain *}
   2.230  
   2.231 @@ -256,14 +256,14 @@
   2.232      by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
   2.233  qed
   2.234  
   2.235 -definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   2.236 -where "prod_sfp = sfp_fun2 prod_approx cprod_map"
   2.237 +definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   2.238 +where "prod_defl = defl_fun2 prod_approx cprod_map"
   2.239  
   2.240 -lemma cast_prod_sfp:
   2.241 -  "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
   2.242 +lemma cast_prod_defl:
   2.243 +  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
   2.244      cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
   2.245 -unfolding prod_sfp_def
   2.246 -apply (rule cast_sfp_fun2 [OF prod_approx])
   2.247 +unfolding prod_defl_def
   2.248 +apply (rule cast_defl_fun2 [OF prod_approx])
   2.249  apply (erule (1) finite_deflation_cprod_map)
   2.250  done
   2.251  
   2.252 @@ -277,7 +277,7 @@
   2.253    "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
   2.254  
   2.255  definition
   2.256 -  "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.257 +  "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.258  
   2.259  instance proof
   2.260    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
   2.261 @@ -285,16 +285,16 @@
   2.262      using ep_pair_udom [OF prod_approx]
   2.263      by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
   2.264  next
   2.265 -  show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
   2.266 -    unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
   2.267 -    by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
   2.268 +  show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
   2.269 +    unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
   2.270 +    by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map)
   2.271  qed
   2.272  
   2.273  end
   2.274  
   2.275 -lemma SFP_prod:
   2.276 -  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.277 -by (rule sfp_prod_def)
   2.278 +lemma DEFL_prod:
   2.279 +  "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.280 +by (rule defl_prod_def)
   2.281  
   2.282  subsection {* Strict product is a bifinite domain *}
   2.283  
   2.284 @@ -315,16 +315,16 @@
   2.285      by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
   2.286  qed
   2.287  
   2.288 -definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   2.289 -where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
   2.290 +definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   2.291 +where "sprod_defl = defl_fun2 sprod_approx sprod_map"
   2.292  
   2.293 -lemma cast_sprod_sfp:
   2.294 -  "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
   2.295 +lemma cast_sprod_defl:
   2.296 +  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
   2.297      udom_emb sprod_approx oo
   2.298        sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
   2.299          udom_prj sprod_approx"
   2.300 -unfolding sprod_sfp_def
   2.301 -apply (rule cast_sfp_fun2 [OF sprod_approx])
   2.302 +unfolding sprod_defl_def
   2.303 +apply (rule cast_defl_fun2 [OF sprod_approx])
   2.304  apply (erule (1) finite_deflation_sprod_map)
   2.305  done
   2.306  
   2.307 @@ -338,7 +338,7 @@
   2.308    "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
   2.309  
   2.310  definition
   2.311 -  "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.312 +  "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.313  
   2.314  instance proof
   2.315    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   2.316 @@ -346,16 +346,16 @@
   2.317      using ep_pair_udom [OF sprod_approx]
   2.318      by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
   2.319  next
   2.320 -  show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   2.321 -    unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
   2.322 -    by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
   2.323 +  show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   2.324 +    unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
   2.325 +    by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map)
   2.326  qed
   2.327  
   2.328  end
   2.329  
   2.330 -lemma SFP_sprod:
   2.331 -  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.332 -by (rule sfp_sprod_def)
   2.333 +lemma DEFL_sprod:
   2.334 +  "DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.335 +by (rule defl_sprod_def)
   2.336  
   2.337  subsection {* Lifted cpo is a bifinite domain *}
   2.338  
   2.339 @@ -374,14 +374,14 @@
   2.340      by (intro finite_deflation_u_map finite_deflation_udom_approx)
   2.341  qed
   2.342  
   2.343 -definition u_sfp :: "sfp \<rightarrow> sfp"
   2.344 -where "u_sfp = sfp_fun1 u_approx u_map"
   2.345 +definition u_defl :: "defl \<rightarrow> defl"
   2.346 +where "u_defl = defl_fun1 u_approx u_map"
   2.347  
   2.348 -lemma cast_u_sfp:
   2.349 -  "cast\<cdot>(u_sfp\<cdot>A) =
   2.350 +lemma cast_u_defl:
   2.351 +  "cast\<cdot>(u_defl\<cdot>A) =
   2.352      udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
   2.353 -unfolding u_sfp_def
   2.354 -apply (rule cast_sfp_fun1 [OF u_approx])
   2.355 +unfolding u_defl_def
   2.356 +apply (rule cast_defl_fun1 [OF u_approx])
   2.357  apply (erule finite_deflation_u_map)
   2.358  done
   2.359  
   2.360 @@ -395,7 +395,7 @@
   2.361    "prj = u_map\<cdot>prj oo udom_prj u_approx"
   2.362  
   2.363  definition
   2.364 -  "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
   2.365 +  "defl (t::'a u itself) = u_defl\<cdot>DEFL('a)"
   2.366  
   2.367  instance proof
   2.368    show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
   2.369 @@ -403,15 +403,15 @@
   2.370      using ep_pair_udom [OF u_approx]
   2.371      by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
   2.372  next
   2.373 -  show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
   2.374 -    unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
   2.375 -    by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
   2.376 +  show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
   2.377 +    unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
   2.378 +    by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map)
   2.379  qed
   2.380  
   2.381  end
   2.382  
   2.383 -lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
   2.384 -by (rule sfp_u_def)
   2.385 +lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>DEFL('a)"
   2.386 +by (rule defl_u_def)
   2.387  
   2.388  subsection {* Lifted countable types are bifinite domains *}
   2.389  
   2.390 @@ -472,25 +472,25 @@
   2.391    "prj = udom_prj lift_approx"
   2.392  
   2.393  definition
   2.394 -  "sfp (t::'a lift itself) =
   2.395 -    (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
   2.396 +  "defl (t::'a lift itself) =
   2.397 +    (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
   2.398  
   2.399  instance proof
   2.400    show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
   2.401      unfolding emb_lift_def prj_lift_def
   2.402      by (rule ep_pair_udom [OF lift_approx])
   2.403 -  show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
   2.404 -    unfolding sfp_lift_def
   2.405 +  show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
   2.406 +    unfolding defl_lift_def
   2.407      apply (subst contlub_cfun_arg)
   2.408      apply (rule chainI)
   2.409 -    apply (rule sfp.principal_mono)
   2.410 +    apply (rule defl.principal_mono)
   2.411      apply (simp add: below_fin_defl_def)
   2.412      apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
   2.413                       ep_pair.finite_deflation_e_d_p [OF ep])
   2.414      apply (intro monofun_cfun below_refl)
   2.415      apply (rule chainE)
   2.416      apply (rule chain_lift_approx)
   2.417 -    apply (subst cast_sfp_principal)
   2.418 +    apply (subst cast_defl_principal)
   2.419      apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
   2.420                       ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
   2.421      done
   2.422 @@ -517,14 +517,14 @@
   2.423      by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
   2.424  qed
   2.425  
   2.426 -definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   2.427 -where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
   2.428 +definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   2.429 +where "ssum_defl = defl_fun2 ssum_approx ssum_map"
   2.430  
   2.431 -lemma cast_ssum_sfp:
   2.432 -  "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
   2.433 +lemma cast_ssum_defl:
   2.434 +  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
   2.435      udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
   2.436 -unfolding ssum_sfp_def
   2.437 -apply (rule cast_sfp_fun2 [OF ssum_approx])
   2.438 +unfolding ssum_defl_def
   2.439 +apply (rule cast_defl_fun2 [OF ssum_approx])
   2.440  apply (erule (1) finite_deflation_ssum_map)
   2.441  done
   2.442  
   2.443 @@ -538,7 +538,7 @@
   2.444    "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
   2.445  
   2.446  definition
   2.447 -  "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.448 +  "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.449  
   2.450  instance proof
   2.451    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   2.452 @@ -546,15 +546,15 @@
   2.453      using ep_pair_udom [OF ssum_approx]
   2.454      by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
   2.455  next
   2.456 -  show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   2.457 -    unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
   2.458 -    by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
   2.459 +  show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   2.460 +    unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
   2.461 +    by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map)
   2.462  qed
   2.463  
   2.464  end
   2.465  
   2.466 -lemma SFP_ssum:
   2.467 -  "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.468 -by (rule sfp_ssum_def)
   2.469 +lemma DEFL_ssum:
   2.470 +  "DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
   2.471 +by (rule defl_ssum_def)
   2.472  
   2.473  end
     3.1 --- a/src/HOLCF/ConvexPD.thy	Mon Oct 11 07:09:42 2010 -0700
     3.2 +++ b/src/HOLCF/ConvexPD.thy	Mon Oct 11 08:32:09 2010 -0700
     3.3 @@ -463,14 +463,14 @@
     3.4      by (intro finite_deflation_convex_map finite_deflation_udom_approx)
     3.5  qed
     3.6  
     3.7 -definition convex_sfp :: "sfp \<rightarrow> sfp"
     3.8 -where "convex_sfp = sfp_fun1 convex_approx convex_map"
     3.9 +definition convex_defl :: "defl \<rightarrow> defl"
    3.10 +where "convex_defl = defl_fun1 convex_approx convex_map"
    3.11  
    3.12 -lemma cast_convex_sfp:
    3.13 -  "cast\<cdot>(convex_sfp\<cdot>A) =
    3.14 +lemma cast_convex_defl:
    3.15 +  "cast\<cdot>(convex_defl\<cdot>A) =
    3.16      udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
    3.17 -unfolding convex_sfp_def
    3.18 -apply (rule cast_sfp_fun1 [OF convex_approx])
    3.19 +unfolding convex_defl_def
    3.20 +apply (rule cast_defl_fun1 [OF convex_approx])
    3.21  apply (erule finite_deflation_convex_map)
    3.22  done
    3.23  
    3.24 @@ -484,7 +484,7 @@
    3.25    "prj = convex_map\<cdot>prj oo udom_prj convex_approx"
    3.26  
    3.27  definition
    3.28 -  "sfp (t::'a convex_pd itself) = convex_sfp\<cdot>SFP('a)"
    3.29 +  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
    3.30  
    3.31  instance proof
    3.32    show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
    3.33 @@ -492,17 +492,17 @@
    3.34      using ep_pair_udom [OF convex_approx]
    3.35      by (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj)
    3.36  next
    3.37 -  show "cast\<cdot>SFP('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
    3.38 -    unfolding emb_convex_pd_def prj_convex_pd_def sfp_convex_pd_def cast_convex_sfp
    3.39 -    by (simp add: cast_SFP oo_def expand_cfun_eq convex_map_map)
    3.40 +  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
    3.41 +    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
    3.42 +    by (simp add: cast_DEFL oo_def expand_cfun_eq convex_map_map)
    3.43  qed
    3.44  
    3.45  end
    3.46  
    3.47 -text {* SFP of type constructor = type combinator *}
    3.48 +text {* DEFL of type constructor = type combinator *}
    3.49  
    3.50 -lemma SFP_convex: "SFP('a convex_pd) = convex_sfp\<cdot>SFP('a)"
    3.51 -by (rule sfp_convex_pd_def)
    3.52 +lemma DEFL_convex: "DEFL('a convex_pd) = convex_defl\<cdot>DEFL('a)"
    3.53 +by (rule defl_convex_pd_def)
    3.54  
    3.55  
    3.56  subsection {* Join *}
     4.1 --- a/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 07:09:42 2010 -0700
     4.2 +++ b/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 08:32:09 2010 -0700
     4.3 @@ -162,14 +162,14 @@
     4.4      by (intro finite_deflation_sfun_map finite_deflation_udom_approx)
     4.5  qed
     4.6  
     4.7 -definition sfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
     4.8 -where "sfun_sfp = sfp_fun2 sfun_approx sfun_map"
     4.9 +definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    4.10 +where "sfun_defl = defl_fun2 sfun_approx sfun_map"
    4.11  
    4.12 -lemma cast_sfun_sfp:
    4.13 -  "cast\<cdot>(sfun_sfp\<cdot>A\<cdot>B) =
    4.14 +lemma cast_sfun_defl:
    4.15 +  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
    4.16      udom_emb sfun_approx oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj sfun_approx"
    4.17 -unfolding sfun_sfp_def
    4.18 -apply (rule cast_sfp_fun2 [OF sfun_approx])
    4.19 +unfolding sfun_defl_def
    4.20 +apply (rule cast_defl_fun2 [OF sfun_approx])
    4.21  apply (erule (1) finite_deflation_sfun_map)
    4.22  done
    4.23  
    4.24 @@ -183,7 +183,7 @@
    4.25    "prj = sfun_map\<cdot>emb\<cdot>prj oo udom_prj sfun_approx"
    4.26  
    4.27  definition
    4.28 -  "sfp (t::('a \<rightarrow>! 'b) itself) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    4.29 +  "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
    4.30  
    4.31  instance proof
    4.32    show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
    4.33 @@ -191,29 +191,29 @@
    4.34      using ep_pair_udom [OF sfun_approx]
    4.35      by (intro ep_pair_comp ep_pair_sfun_map ep_pair_emb_prj)
    4.36  next
    4.37 -  show "cast\<cdot>SFP('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
    4.38 -    unfolding emb_sfun_def prj_sfun_def sfp_sfun_def cast_sfun_sfp
    4.39 -    by (simp add: cast_SFP oo_def expand_cfun_eq sfun_map_map)
    4.40 +  show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
    4.41 +    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
    4.42 +    by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
    4.43  qed
    4.44  
    4.45  end
    4.46  
    4.47 -lemma SFP_sfun:
    4.48 -  "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    4.49 -by (rule sfp_sfun_def)
    4.50 +lemma DEFL_sfun:
    4.51 +  "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
    4.52 +by (rule defl_sfun_def)
    4.53  
    4.54  lemma isodefl_sfun:
    4.55    "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
    4.56 -    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_sfp\<cdot>t1\<cdot>t2)"
    4.57 +    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
    4.58  apply (rule isodeflI)
    4.59 -apply (simp add: cast_sfun_sfp cast_isodefl)
    4.60 +apply (simp add: cast_sfun_defl cast_isodefl)
    4.61  apply (simp add: emb_sfun_def prj_sfun_def)
    4.62  apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation])
    4.63  done
    4.64  
    4.65  setup {*
    4.66    Domain_Isomorphism.add_type_constructor
    4.67 -    (@{type_name "sfun"}, @{term sfun_sfp}, @{const_name sfun_map}, @{thm SFP_sfun},
    4.68 +    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm DEFL_sfun},
    4.69         @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
    4.70  *}
    4.71  
     5.1 --- a/src/HOLCF/LowerPD.thy	Mon Oct 11 07:09:42 2010 -0700
     5.2 +++ b/src/HOLCF/LowerPD.thy	Mon Oct 11 08:32:09 2010 -0700
     5.3 @@ -452,14 +452,14 @@
     5.4      by (intro finite_deflation_lower_map finite_deflation_udom_approx)
     5.5  qed
     5.6  
     5.7 -definition lower_sfp :: "sfp \<rightarrow> sfp"
     5.8 -where "lower_sfp = sfp_fun1 lower_approx lower_map"
     5.9 +definition lower_defl :: "defl \<rightarrow> defl"
    5.10 +where "lower_defl = defl_fun1 lower_approx lower_map"
    5.11  
    5.12 -lemma cast_lower_sfp:
    5.13 -  "cast\<cdot>(lower_sfp\<cdot>A) =
    5.14 +lemma cast_lower_defl:
    5.15 +  "cast\<cdot>(lower_defl\<cdot>A) =
    5.16      udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
    5.17 -unfolding lower_sfp_def
    5.18 -apply (rule cast_sfp_fun1 [OF lower_approx])
    5.19 +unfolding lower_defl_def
    5.20 +apply (rule cast_defl_fun1 [OF lower_approx])
    5.21  apply (erule finite_deflation_lower_map)
    5.22  done
    5.23  
    5.24 @@ -473,7 +473,7 @@
    5.25    "prj = lower_map\<cdot>prj oo udom_prj lower_approx"
    5.26  
    5.27  definition
    5.28 -  "sfp (t::'a lower_pd itself) = lower_sfp\<cdot>SFP('a)"
    5.29 +  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
    5.30  
    5.31  instance proof
    5.32    show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
    5.33 @@ -481,15 +481,15 @@
    5.34      using ep_pair_udom [OF lower_approx]
    5.35      by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj)
    5.36  next
    5.37 -  show "cast\<cdot>SFP('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
    5.38 -    unfolding emb_lower_pd_def prj_lower_pd_def sfp_lower_pd_def cast_lower_sfp
    5.39 -    by (simp add: cast_SFP oo_def expand_cfun_eq lower_map_map)
    5.40 +  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
    5.41 +    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
    5.42 +    by (simp add: cast_DEFL oo_def expand_cfun_eq lower_map_map)
    5.43  qed
    5.44  
    5.45  end
    5.46  
    5.47 -lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
    5.48 -by (rule sfp_lower_pd_def)
    5.49 +lemma DEFL_lower: "DEFL('a lower_pd) = lower_defl\<cdot>DEFL('a)"
    5.50 +by (rule defl_lower_pd_def)
    5.51  
    5.52  
    5.53  subsection {* Join *}
     6.1 --- a/src/HOLCF/Powerdomains.thy	Mon Oct 11 07:09:42 2010 -0700
     6.2 +++ b/src/HOLCF/Powerdomains.thy	Mon Oct 11 08:32:09 2010 -0700
     6.3 @@ -9,25 +9,25 @@
     6.4  begin
     6.5  
     6.6  lemma isodefl_upper:
     6.7 -  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_sfp\<cdot>t)"
     6.8 +  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
     6.9  apply (rule isodeflI)
    6.10 -apply (simp add: cast_upper_sfp cast_isodefl)
    6.11 +apply (simp add: cast_upper_defl cast_isodefl)
    6.12  apply (simp add: emb_upper_pd_def prj_upper_pd_def)
    6.13  apply (simp add: upper_map_map)
    6.14  done
    6.15  
    6.16  lemma isodefl_lower:
    6.17 -  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_sfp\<cdot>t)"
    6.18 +  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
    6.19  apply (rule isodeflI)
    6.20 -apply (simp add: cast_lower_sfp cast_isodefl)
    6.21 +apply (simp add: cast_lower_defl cast_isodefl)
    6.22  apply (simp add: emb_lower_pd_def prj_lower_pd_def)
    6.23  apply (simp add: lower_map_map)
    6.24  done
    6.25  
    6.26  lemma isodefl_convex:
    6.27 -  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_sfp\<cdot>t)"
    6.28 +  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
    6.29  apply (rule isodeflI)
    6.30 -apply (simp add: cast_convex_sfp cast_isodefl)
    6.31 +apply (simp add: cast_convex_defl cast_isodefl)
    6.32  apply (simp add: emb_convex_pd_def prj_convex_pd_def)
    6.33  apply (simp add: convex_map_map)
    6.34  done
    6.35 @@ -36,16 +36,16 @@
    6.36  
    6.37  setup {*
    6.38    fold Domain_Isomorphism.add_type_constructor
    6.39 -    [(@{type_name "upper_pd"}, @{term upper_sfp}, @{const_name upper_map},
    6.40 -        @{thm SFP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
    6.41 +    [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
    6.42 +        @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
    6.43            @{thm deflation_upper_map}),
    6.44  
    6.45 -     (@{type_name "lower_pd"}, @{term lower_sfp}, @{const_name lower_map},
    6.46 -        @{thm SFP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
    6.47 +     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
    6.48 +        @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
    6.49            @{thm deflation_lower_map}),
    6.50  
    6.51 -     (@{type_name "convex_pd"}, @{term convex_sfp}, @{const_name convex_map},
    6.52 -        @{thm SFP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
    6.53 +     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
    6.54 +        @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
    6.55            @{thm deflation_convex_map})]
    6.56  *}
    6.57  
     7.1 --- a/src/HOLCF/Representable.thy	Mon Oct 11 07:09:42 2010 -0700
     7.2 +++ b/src/HOLCF/Representable.thy	Mon Oct 11 08:32:09 2010 -0700
     7.3 @@ -15,20 +15,20 @@
     7.4  
     7.5  subsection {* Representations of types *}
     7.6  
     7.7 -lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
     7.8 -by (simp add: cast_SFP)
     7.9 +lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
    7.10 +by (simp add: cast_DEFL)
    7.11  
    7.12 -lemma in_SFP_iff:
    7.13 -  "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    7.14 -by (simp add: in_sfp_def cast_SFP)
    7.15 +lemma in_DEFL_iff:
    7.16 +  "x ::: DEFL('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    7.17 +by (simp add: in_defl_def cast_DEFL)
    7.18  
    7.19  lemma prj_inverse:
    7.20 -  "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    7.21 -by (simp only: in_SFP_iff)
    7.22 +  "x ::: DEFL('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
    7.23 +by (simp only: in_DEFL_iff)
    7.24  
    7.25 -lemma emb_in_SFP [simp]:
    7.26 -  "emb\<cdot>(x::'a) ::: SFP('a)"
    7.27 -by (simp add: in_SFP_iff)
    7.28 +lemma emb_in_DEFL [simp]:
    7.29 +  "emb\<cdot>(x::'a) ::: DEFL('a)"
    7.30 +by (simp add: in_DEFL_iff)
    7.31  
    7.32  subsection {* Coerce operator *}
    7.33  
    7.34 @@ -48,16 +48,16 @@
    7.35  by (rule ext_cfun, simp add: beta_coerce)
    7.36  
    7.37  lemma emb_coerce:
    7.38 -  "SFP('a) \<sqsubseteq> SFP('b)
    7.39 +  "DEFL('a) \<sqsubseteq> DEFL('b)
    7.40     \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
    7.41   apply (simp add: beta_coerce)
    7.42   apply (rule prj_inverse)
    7.43 - apply (erule sfp_belowD)
    7.44 - apply (rule emb_in_SFP)
    7.45 + apply (erule defl_belowD)
    7.46 + apply (rule emb_in_DEFL)
    7.47  done
    7.48  
    7.49  lemma coerce_prj:
    7.50 -  "SFP('a) \<sqsubseteq> SFP('b)
    7.51 +  "DEFL('a) \<sqsubseteq> DEFL('b)
    7.52     \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
    7.53   apply (simp add: coerce_def)
    7.54   apply (rule emb_eq_iff [THEN iffD1])
    7.55 @@ -69,21 +69,21 @@
    7.56  done
    7.57  
    7.58  lemma coerce_coerce [simp]:
    7.59 -  "SFP('a) \<sqsubseteq> SFP('b)
    7.60 +  "DEFL('a) \<sqsubseteq> DEFL('b)
    7.61     \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
    7.62 -by (simp add: beta_coerce prj_inverse sfp_belowD)
    7.63 +by (simp add: beta_coerce prj_inverse defl_belowD)
    7.64  
    7.65  lemma coerce_inverse:
    7.66 -  "emb\<cdot>(x::'a) ::: SFP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
    7.67 +  "emb\<cdot>(x::'a) ::: DEFL('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
    7.68  by (simp only: beta_coerce prj_inverse emb_inverse)
    7.69  
    7.70  lemma coerce_type:
    7.71 -  "SFP('a) \<sqsubseteq> SFP('b)
    7.72 -   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: SFP('a)"
    7.73 -by (simp add: beta_coerce prj_inverse sfp_belowD)
    7.74 +  "DEFL('a) \<sqsubseteq> DEFL('b)
    7.75 +   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: DEFL('a)"
    7.76 +by (simp add: beta_coerce prj_inverse defl_belowD)
    7.77  
    7.78  lemma ep_pair_coerce:
    7.79 -  "SFP('a) \<sqsubseteq> SFP('b)
    7.80 +  "DEFL('a) \<sqsubseteq> DEFL('b)
    7.81     \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
    7.82   apply (rule ep_pair.intro)
    7.83    apply simp
    7.84 @@ -98,19 +98,19 @@
    7.85  
    7.86  lemma domain_abs_iso:
    7.87    fixes abs and rep
    7.88 -  assumes SFP: "SFP('b) = SFP('a)"
    7.89 +  assumes DEFL: "DEFL('b) = DEFL('a)"
    7.90    assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
    7.91    assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
    7.92    shows "rep\<cdot>(abs\<cdot>x) = x"
    7.93 -unfolding abs_def rep_def by (simp add: SFP)
    7.94 +unfolding abs_def rep_def by (simp add: DEFL)
    7.95  
    7.96  lemma domain_rep_iso:
    7.97    fixes abs and rep
    7.98 -  assumes SFP: "SFP('b) = SFP('a)"
    7.99 +  assumes DEFL: "DEFL('b) = DEFL('a)"
   7.100    assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   7.101    assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   7.102    shows "abs\<cdot>(rep\<cdot>x) = x"
   7.103 -unfolding abs_def rep_def by (simp add: SFP [symmetric])
   7.104 +unfolding abs_def rep_def by (simp add: DEFL [symmetric])
   7.105  
   7.106  
   7.107  subsection {* Proving a subtype is representable *}
   7.108 @@ -120,7 +120,7 @@
   7.109  *}
   7.110  
   7.111  setup {* Sign.add_const_constraint
   7.112 -  (@{const_name sfp}, SOME @{typ "'a::pcpo itself \<Rightarrow> sfp"}) *}
   7.113 +  (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"}) *}
   7.114  
   7.115  setup {* Sign.add_const_constraint
   7.116    (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
   7.117 @@ -131,16 +131,16 @@
   7.118  lemma typedef_rep_class:
   7.119    fixes Rep :: "'a::pcpo \<Rightarrow> udom"
   7.120    fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
   7.121 -  fixes t :: sfp
   7.122 +  fixes t :: defl
   7.123    assumes type: "type_definition Rep Abs {x. x ::: t}"
   7.124    assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   7.125    assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
   7.126    assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
   7.127 -  assumes sfp: "sfp \<equiv> (\<lambda> a::'a itself. t)"
   7.128 +  assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
   7.129    shows "OFCLASS('a, bifinite_class)"
   7.130  proof
   7.131    have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
   7.132 -    by (simp add: adm_in_sfp)
   7.133 +    by (simp add: adm_in_defl)
   7.134    have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
   7.135      unfolding emb
   7.136      apply (rule beta_cfun)
   7.137 @@ -152,12 +152,12 @@
   7.138      apply (rule typedef_cont_Abs [OF type below adm])
   7.139      apply simp_all
   7.140      done
   7.141 -  have emb_in_sfp: "\<And>x::'a. emb\<cdot>x ::: t"
   7.142 +  have emb_in_defl: "\<And>x::'a. emb\<cdot>x ::: t"
   7.143      using type_definition.Rep [OF type]
   7.144      by (simp add: emb_beta)
   7.145    have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
   7.146      unfolding prj_beta
   7.147 -    apply (simp add: cast_fixed [OF emb_in_sfp])
   7.148 +    apply (simp add: cast_fixed [OF emb_in_defl])
   7.149      apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
   7.150      done
   7.151    have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
   7.152 @@ -168,19 +168,19 @@
   7.153      apply (simp add: prj_emb)
   7.154      apply (simp add: emb_prj cast.below)
   7.155      done
   7.156 -  show "cast\<cdot>SFP('a) = emb oo (prj :: udom \<rightarrow> 'a)"
   7.157 -    by (rule ext_cfun, simp add: sfp emb_prj)
   7.158 +  show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
   7.159 +    by (rule ext_cfun, simp add: defl emb_prj)
   7.160  qed
   7.161  
   7.162 -lemma typedef_SFP:
   7.163 -  assumes "sfp \<equiv> (\<lambda>a::'a::pcpo itself. t)"
   7.164 -  shows "SFP('a::pcpo) = t"
   7.165 +lemma typedef_DEFL:
   7.166 +  assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
   7.167 +  shows "DEFL('a::pcpo) = t"
   7.168  unfolding assms ..
   7.169  
   7.170  text {* Restore original typing constraints *}
   7.171  
   7.172  setup {* Sign.add_const_constraint
   7.173 -  (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
   7.174 +  (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) *}
   7.175  
   7.176  setup {* Sign.add_const_constraint
   7.177    (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
   7.178 @@ -188,15 +188,15 @@
   7.179  setup {* Sign.add_const_constraint
   7.180    (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
   7.181  
   7.182 -lemma adm_mem_Collect_in_sfp: "adm (\<lambda>x. x \<in> {x. x ::: A})"
   7.183 -unfolding mem_Collect_eq by (rule adm_in_sfp)
   7.184 +lemma adm_mem_Collect_in_defl: "adm (\<lambda>x. x \<in> {x. x ::: A})"
   7.185 +unfolding mem_Collect_eq by (rule adm_in_defl)
   7.186  
   7.187  use "Tools/repdef.ML"
   7.188  
   7.189  subsection {* Isomorphic deflations *}
   7.190  
   7.191  definition
   7.192 -  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
   7.193 +  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
   7.194  where
   7.195    "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
   7.196  
   7.197 @@ -222,12 +222,12 @@
   7.198      using cast.below [of t "emb\<cdot>x"] by simp
   7.199  qed
   7.200  
   7.201 -lemma isodefl_ID_SFP: "isodefl (ID :: 'a \<rightarrow> 'a) SFP('a)"
   7.202 -unfolding isodefl_def by (simp add: cast_SFP)
   7.203 +lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
   7.204 +unfolding isodefl_def by (simp add: cast_DEFL)
   7.205  
   7.206 -lemma isodefl_SFP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) SFP('a) \<Longrightarrow> d = ID"
   7.207 +lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
   7.208  unfolding isodefl_def
   7.209 -apply (simp add: cast_SFP)
   7.210 +apply (simp add: cast_DEFL)
   7.211  apply (simp add: expand_cfun_eq)
   7.212  apply (rule allI)
   7.213  apply (drule_tac x="emb\<cdot>x" in spec)
   7.214 @@ -260,61 +260,61 @@
   7.215  
   7.216  lemma isodefl_coerce:
   7.217    fixes d :: "'a \<rightarrow> 'a"
   7.218 -  assumes SFP: "SFP('b) = SFP('a)"
   7.219 +  assumes DEFL: "DEFL('b) = DEFL('a)"
   7.220    shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
   7.221  unfolding isodefl_def
   7.222  apply (simp add: expand_cfun_eq)
   7.223 -apply (simp add: emb_coerce coerce_prj SFP)
   7.224 +apply (simp add: emb_coerce coerce_prj DEFL)
   7.225  done
   7.226  
   7.227  lemma isodefl_abs_rep:
   7.228    fixes abs and rep and d
   7.229 -  assumes SFP: "SFP('b) = SFP('a)"
   7.230 +  assumes DEFL: "DEFL('b) = DEFL('a)"
   7.231    assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
   7.232    assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
   7.233    shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
   7.234 -unfolding abs_def rep_def using SFP by (rule isodefl_coerce)
   7.235 +unfolding abs_def rep_def using DEFL by (rule isodefl_coerce)
   7.236  
   7.237  lemma isodefl_cfun:
   7.238    "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   7.239 -    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_sfp\<cdot>t1\<cdot>t2)"
   7.240 +    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
   7.241  apply (rule isodeflI)
   7.242 -apply (simp add: cast_cfun_sfp cast_isodefl)
   7.243 +apply (simp add: cast_cfun_defl cast_isodefl)
   7.244  apply (simp add: emb_cfun_def prj_cfun_def)
   7.245  apply (simp add: cfun_map_map cfcomp1)
   7.246  done
   7.247  
   7.248  lemma isodefl_ssum:
   7.249    "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   7.250 -    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_sfp\<cdot>t1\<cdot>t2)"
   7.251 +    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
   7.252  apply (rule isodeflI)
   7.253 -apply (simp add: cast_ssum_sfp cast_isodefl)
   7.254 +apply (simp add: cast_ssum_defl cast_isodefl)
   7.255  apply (simp add: emb_ssum_def prj_ssum_def)
   7.256  apply (simp add: ssum_map_map isodefl_strict)
   7.257  done
   7.258  
   7.259  lemma isodefl_sprod:
   7.260    "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   7.261 -    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_sfp\<cdot>t1\<cdot>t2)"
   7.262 +    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
   7.263  apply (rule isodeflI)
   7.264 -apply (simp add: cast_sprod_sfp cast_isodefl)
   7.265 +apply (simp add: cast_sprod_defl cast_isodefl)
   7.266  apply (simp add: emb_sprod_def prj_sprod_def)
   7.267  apply (simp add: sprod_map_map isodefl_strict)
   7.268  done
   7.269  
   7.270  lemma isodefl_cprod:
   7.271    "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
   7.272 -    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_sfp\<cdot>t1\<cdot>t2)"
   7.273 +    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
   7.274  apply (rule isodeflI)
   7.275 -apply (simp add: cast_prod_sfp cast_isodefl)
   7.276 +apply (simp add: cast_prod_defl cast_isodefl)
   7.277  apply (simp add: emb_prod_def prj_prod_def)
   7.278  apply (simp add: cprod_map_map cfcomp1)
   7.279  done
   7.280  
   7.281  lemma isodefl_u:
   7.282 -  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_sfp\<cdot>t)"
   7.283 +  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
   7.284  apply (rule isodeflI)
   7.285 -apply (simp add: cast_u_sfp cast_isodefl)
   7.286 +apply (simp add: cast_u_defl cast_isodefl)
   7.287  apply (simp add: emb_u_def prj_u_def)
   7.288  apply (simp add: u_map_map)
   7.289  done
   7.290 @@ -325,19 +325,19 @@
   7.291  
   7.292  setup {*
   7.293    fold Domain_Isomorphism.add_type_constructor
   7.294 -    [(@{type_name cfun}, @{term cfun_sfp}, @{const_name cfun_map}, @{thm SFP_cfun},
   7.295 +    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
   7.296          @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
   7.297  
   7.298 -     (@{type_name ssum}, @{term ssum_sfp}, @{const_name ssum_map}, @{thm SFP_ssum},
   7.299 +     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
   7.300          @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
   7.301  
   7.302 -     (@{type_name sprod}, @{term sprod_sfp}, @{const_name sprod_map}, @{thm SFP_sprod},
   7.303 +     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
   7.304          @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
   7.305  
   7.306 -     (@{type_name prod}, @{term cprod_sfp}, @{const_name cprod_map}, @{thm SFP_prod},
   7.307 +     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
   7.308          @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
   7.309  
   7.310 -     (@{type_name "u"}, @{term u_sfp}, @{const_name u_map}, @{thm SFP_u},
   7.311 +     (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
   7.312          @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
   7.313  *}
   7.314  
     8.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Oct 11 07:09:42 2010 -0700
     8.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Oct 11 08:32:09 2010 -0700
     8.3 @@ -48,7 +48,7 @@
     8.4  
     8.5  structure DeflData = Theory_Data
     8.6  (
     8.7 -  (* terms like "foo_sfp" *)
     8.8 +  (* terms like "foo_defl" *)
     8.9    type T = term Symtab.table;
    8.10    val empty = Symtab.empty;
    8.11    val extend = I;
    8.12 @@ -57,7 +57,7 @@
    8.13  
    8.14  structure RepData = Theory_Data
    8.15  (
    8.16 -  (* theorems like "SFP('a foo) = foo_sfp$SFP('a)" *)
    8.17 +  (* theorems like "DEFL('a foo) = foo_defl$DEFL('a)" *)
    8.18    type T = thm list;
    8.19    val empty = [];
    8.20    val extend = I;
    8.21 @@ -83,11 +83,11 @@
    8.22  );
    8.23  
    8.24  fun add_type_constructor
    8.25 -  (tname, defl_const, map_name, SFP_thm,
    8.26 +  (tname, defl_const, map_name, DEFL_thm,
    8.27     isodefl_thm, map_ID_thm, defl_map_thm) =
    8.28      DeflData.map (Symtab.insert (K true) (tname, defl_const))
    8.29      #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
    8.30 -    #> RepData.map (Thm.add_thm SFP_thm)
    8.31 +    #> RepData.map (Thm.add_thm DEFL_thm)
    8.32      #> IsodeflData.map (Thm.add_thm isodefl_thm)
    8.33      #> MapIdData.map (Thm.add_thm map_ID_thm);
    8.34  
    8.35 @@ -104,19 +104,19 @@
    8.36  infixr 6 ->>;
    8.37  infix -->>;
    8.38  
    8.39 -val sfpT = @{typ "sfp"};
    8.40 +val deflT = @{typ "defl"};
    8.41  
    8.42  fun mapT (T as Type (_, Ts)) =
    8.43      (map (fn T => T ->> T) Ts) -->> (T ->> T)
    8.44    | mapT T = T ->> T;
    8.45  
    8.46 -fun mk_SFP T =
    8.47 -  Const (@{const_name sfp}, Term.itselfT T --> sfpT) $ Logic.mk_type T;
    8.48 +fun mk_DEFL T =
    8.49 +  Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
    8.50  
    8.51  fun coerce_const T = Const (@{const_name coerce}, T);
    8.52  
    8.53  fun isodefl_const T =
    8.54 -  Const (@{const_name isodefl}, (T ->> T) --> sfpT --> HOLogic.boolT);
    8.55 +  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
    8.56  
    8.57  fun mk_deflation t =
    8.58    Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
    8.59 @@ -218,13 +218,13 @@
    8.60    let
    8.61      fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
    8.62        | is_closed_typ _ = false;
    8.63 -    fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, sfpT)
    8.64 +    fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
    8.65        | defl_of (TVar _) = error ("defl_of_typ: TVar")
    8.66        | defl_of (T as Type (c, Ts)) =
    8.67          case Symtab.lookup tab c of
    8.68            SOME t => list_ccomb (t, map defl_of Ts)
    8.69          | NONE => if is_closed_typ T
    8.70 -                  then mk_SFP T
    8.71 +                  then mk_DEFL T
    8.72                    else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
    8.73    in defl_of T end;
    8.74  
    8.75 @@ -443,7 +443,7 @@
    8.76      (* declare deflation combinator constants *)
    8.77      fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
    8.78        let
    8.79 -        val defl_type = map (K sfpT) vs -->> sfpT;
    8.80 +        val defl_type = map (K deflT) vs -->> deflT;
    8.81          val defl_bind = Binding.suffix_name "_defl" tbind;
    8.82        in
    8.83          Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
    8.84 @@ -470,34 +470,34 @@
    8.85      fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
    8.86        let
    8.87          fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
    8.88 -        val reps = map (mk_SFP o tfree) vs;
    8.89 +        val reps = map (mk_DEFL o tfree) vs;
    8.90          val defl = list_ccomb (defl_const, reps);
    8.91 -        val ((_, _, _, {SFP, ...}), thy) =
    8.92 +        val ((_, _, _, {DEFL, ...}), thy) =
    8.93            Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
    8.94        in
    8.95 -        (SFP, thy)
    8.96 +        (DEFL, thy)
    8.97        end;
    8.98 -    val (SFP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
    8.99 -    val thy = RepData.map (fold Thm.add_thm SFP_thms) thy;
   8.100 +    val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
   8.101 +    val thy = RepData.map (fold Thm.add_thm DEFL_thms) thy;
   8.102  
   8.103 -    (* prove SFP equations *)
   8.104 -    fun mk_SFP_eq_thm (lhsT, rhsT) =
   8.105 +    (* prove DEFL equations *)
   8.106 +    fun mk_DEFL_eq_thm (lhsT, rhsT) =
   8.107        let
   8.108 -        val goal = mk_eqs (mk_SFP lhsT, mk_SFP rhsT);
   8.109 -        val SFP_simps = RepData.get thy;
   8.110 +        val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT);
   8.111 +        val DEFL_simps = RepData.get thy;
   8.112          val tac =
   8.113 -          rewrite_goals_tac (map mk_meta_eq SFP_simps)
   8.114 +          rewrite_goals_tac (map mk_meta_eq DEFL_simps)
   8.115            THEN resolve_tac defl_unfold_thms 1;
   8.116        in
   8.117          Goal.prove_global thy [] [] goal (K tac)
   8.118        end;
   8.119 -    val SFP_eq_thms = map mk_SFP_eq_thm dom_eqns;
   8.120 +    val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns;
   8.121  
   8.122 -    (* register SFP equations *)
   8.123 -    val SFP_eq_binds = map (Binding.prefix_name "SFP_eq_") dbinds;
   8.124 +    (* register DEFL equations *)
   8.125 +    val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds;
   8.126      val (_, thy) = thy |>
   8.127        (Global_Theory.add_thms o map Thm.no_attributes)
   8.128 -        (SFP_eq_binds ~~ SFP_eq_thms);
   8.129 +        (DEFL_eq_binds ~~ DEFL_eq_thms);
   8.130  
   8.131      (* define rep/abs functions *)
   8.132      fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
   8.133 @@ -516,10 +516,10 @@
   8.134        |>> ListPair.unzip;
   8.135  
   8.136      (* prove isomorphism and isodefl rules *)
   8.137 -    fun mk_iso_thms ((tbind, SFP_eq), (rep_def, abs_def)) thy =
   8.138 +    fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy =
   8.139        let
   8.140          fun make thm =
   8.141 -            Drule.zero_var_indexes (thm OF [SFP_eq, abs_def, rep_def]);
   8.142 +            Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def]);
   8.143          val rep_iso_thm = make @{thm domain_rep_iso};
   8.144          val abs_iso_thm = make @{thm domain_abs_iso};
   8.145          val isodefl_thm = make @{thm isodefl_abs_rep};
   8.146 @@ -532,7 +532,7 @@
   8.147        end;
   8.148      val ((iso_thms, isodefl_abs_rep_thms), thy) =
   8.149        thy
   8.150 -      |> fold_map mk_iso_thms (dbinds ~~ SFP_eq_thms ~~ rep_abs_defs)
   8.151 +      |> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs)
   8.152        |>> ListPair.unzip;
   8.153  
   8.154      (* collect info about rep/abs *)
   8.155 @@ -561,7 +561,7 @@
   8.156      val isodefl_thm =
   8.157        let
   8.158          fun unprime a = Library.unprefix "'" a;
   8.159 -        fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), sfpT);
   8.160 +        fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT);
   8.161          fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T);
   8.162          fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T);
   8.163          fun mk_goal ((map_const, defl_const), (T, rhsT)) =
   8.164 @@ -579,9 +579,9 @@
   8.165            @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
   8.166          val bottom_rules =
   8.167            @{thms fst_strict snd_strict isodefl_bottom simp_thms};
   8.168 -        val SFP_simps = map (fn th => th RS sym) (RepData.get thy);
   8.169 +        val DEFL_simps = map (fn th => th RS sym) (RepData.get thy);
   8.170          val isodefl_rules =
   8.171 -          @{thms conjI isodefl_ID_SFP}
   8.172 +          @{thms conjI isodefl_ID_DEFL}
   8.173            @ isodefl_abs_rep_thms
   8.174            @ IsodeflData.get thy;
   8.175        in
   8.176 @@ -595,7 +595,7 @@
   8.177             simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   8.178             simp_tac beta_ss 1,
   8.179             simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
   8.180 -           simp_tac (HOL_basic_ss addsimps SFP_simps) 1,
   8.181 +           simp_tac (HOL_basic_ss addsimps DEFL_simps) 1,
   8.182             REPEAT (etac @{thm conjE} 1),
   8.183             REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
   8.184        end;
   8.185 @@ -613,23 +613,23 @@
   8.186  
   8.187      (* prove map_ID theorems *)
   8.188      fun prove_map_ID_thm
   8.189 -        (((map_const, (lhsT, _)), SFP_thm), isodefl_thm) =
   8.190 +        (((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =
   8.191        let
   8.192          val Ts = snd (dest_Type lhsT);
   8.193          val lhs = list_ccomb (map_const, map mk_ID Ts);
   8.194          val goal = mk_eqs (lhs, mk_ID lhsT);
   8.195          val tac = EVERY
   8.196 -          [rtac @{thm isodefl_SFP_imp_ID} 1,
   8.197 -           stac SFP_thm 1,
   8.198 +          [rtac @{thm isodefl_DEFL_imp_ID} 1,
   8.199 +           stac DEFL_thm 1,
   8.200             rtac isodefl_thm 1,
   8.201 -           REPEAT (rtac @{thm isodefl_ID_SFP} 1)];
   8.202 +           REPEAT (rtac @{thm isodefl_ID_DEFL} 1)];
   8.203        in
   8.204          Goal.prove_global thy [] [] goal (K tac)
   8.205        end;
   8.206      val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds;
   8.207      val map_ID_thms =
   8.208        map prove_map_ID_thm
   8.209 -        (map_consts ~~ dom_eqns ~~ SFP_thms ~~ isodefl_thms);
   8.210 +        (map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms);
   8.211      val (_, thy) = thy |>
   8.212        (Global_Theory.add_thms o map Thm.no_attributes)
   8.213          (map_ID_binds ~~ map_ID_thms);
     9.1 --- a/src/HOLCF/Tools/repdef.ML	Mon Oct 11 07:09:42 2010 -0700
     9.2 +++ b/src/HOLCF/Tools/repdef.ML	Mon Oct 11 08:32:09 2010 -0700
     9.3 @@ -7,7 +7,7 @@
     9.4  signature REPDEF =
     9.5  sig
     9.6    type rep_info =
     9.7 -    { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm }
     9.8 +    { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm }
     9.9  
    9.10    val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    9.11      term -> (binding * binding) option -> theory ->
    9.12 @@ -28,19 +28,19 @@
    9.13  (** type definitions **)
    9.14  
    9.15  type rep_info =
    9.16 -  { emb_def: thm, prj_def: thm, sfp_def: thm, SFP: thm };
    9.17 +  { emb_def: thm, prj_def: thm, defl_def: thm, DEFL: thm };
    9.18  
    9.19  (* building types and terms *)
    9.20  
    9.21  val udomT = @{typ udom};
    9.22 -val sfpT = @{typ sfp};
    9.23 +val deflT = @{typ defl};
    9.24  fun emb_const T = Const (@{const_name emb}, T ->> udomT);
    9.25  fun prj_const T = Const (@{const_name prj}, udomT ->> T);
    9.26 -fun sfp_const T = Const (@{const_name sfp}, Term.itselfT T --> sfpT);
    9.27 +fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT);
    9.28  
    9.29  fun mk_cast (t, x) =
    9.30    capply_const (udomT, udomT)
    9.31 -  $ (capply_const (sfpT, udomT ->> udomT) $ @{const cast} $ t)
    9.32 +  $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
    9.33    $ x;
    9.34  
    9.35  (* manipulating theorems *)
    9.36 @@ -70,8 +70,8 @@
    9.37      val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
    9.38  
    9.39      val deflT = Term.fastype_of defl;
    9.40 -    val _ = if deflT = @{typ "sfp"} then ()
    9.41 -            else error ("Not type sfp: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
    9.42 +    val _ = if deflT = @{typ "defl"} then ()
    9.43 +            else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
    9.44  
    9.45      (*lhs*)
    9.46      val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
    9.47 @@ -84,12 +84,12 @@
    9.48        |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
    9.49  
    9.50      (*set*)
    9.51 -    val in_defl = @{term "in_sfp :: udom => sfp => bool"};
    9.52 +    val in_defl = @{term "in_defl :: udom => defl => bool"};
    9.53      val set = HOLogic.Collect_const udomT $ Abs ("x", udomT, in_defl $ Bound 0 $ defl);
    9.54  
    9.55      (*pcpodef*)
    9.56 -    val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_sfp} 1;
    9.57 -    val tac2 = rtac @{thm adm_mem_Collect_in_sfp} 1;
    9.58 +    val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_defl} 1;
    9.59 +    val tac2 = rtac @{thm adm_mem_Collect_in_defl} 1;
    9.60      val ((info, cpo_info, pcpo_info), thy) = thy
    9.61        |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
    9.62  
    9.63 @@ -99,12 +99,12 @@
    9.64      val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
    9.65      val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
    9.66        Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
    9.67 -    val sfp_eqn = Logic.mk_equals (sfp_const newT,
    9.68 +    val defl_eqn = Logic.mk_equals (defl_const newT,
    9.69        Abs ("x", Term.itselfT newT, defl));
    9.70      val name_def = Binding.suffix_name "_def" name;
    9.71      val emb_bind = (Binding.prefix_name "emb_" name_def, []);
    9.72      val prj_bind = (Binding.prefix_name "prj_" name_def, []);
    9.73 -    val sfp_bind = (Binding.prefix_name "sfp_" name_def, []);
    9.74 +    val defl_bind = (Binding.prefix_name "defl_" name_def, []);
    9.75  
    9.76      (*instantiate class rep*)
    9.77      val lthy = thy
    9.78 @@ -113,34 +113,34 @@
    9.79          Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
    9.80      val ((_, (_, prj_ldef)), lthy) =
    9.81          Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
    9.82 -    val ((_, (_, sfp_ldef)), lthy) =
    9.83 -        Specification.definition (NONE, (sfp_bind, sfp_eqn)) lthy;
    9.84 +    val ((_, (_, defl_ldef)), lthy) =
    9.85 +        Specification.definition (NONE, (defl_bind, defl_eqn)) lthy;
    9.86      val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
    9.87      val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
    9.88      val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
    9.89 -    val sfp_def = singleton (ProofContext.export lthy ctxt_thy) sfp_ldef;
    9.90 +    val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef;
    9.91      val type_definition_thm =
    9.92        MetaSimplifier.rewrite_rule
    9.93          (the_list (#set_def (#2 info)))
    9.94          (#type_definition (#2 info));
    9.95      val typedef_thms =
    9.96 -      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, sfp_def];
    9.97 +      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def];
    9.98      val thy = lthy
    9.99        |> Class.prove_instantiation_instance
   9.100            (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
   9.101        |> Local_Theory.exit_global;
   9.102  
   9.103      (*other theorems*)
   9.104 -    val sfp_thm' = Thm.transfer thy sfp_def;
   9.105 -    val (SFP_thm, thy) = thy
   9.106 +    val defl_thm' = Thm.transfer thy defl_def;
   9.107 +    val (DEFL_thm, thy) = thy
   9.108        |> Sign.add_path (Binding.name_of name)
   9.109        |> Global_Theory.add_thm
   9.110 -         ((Binding.prefix_name "SFP_" name,
   9.111 -          Drule.zero_var_indexes (@{thm typedef_SFP} OF [sfp_thm'])), [])
   9.112 +         ((Binding.prefix_name "DEFL_" name,
   9.113 +          Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
   9.114        ||> Sign.restore_naming thy;
   9.115  
   9.116      val rep_info =
   9.117 -      { emb_def = emb_def, prj_def = prj_def, sfp_def = sfp_def, SFP = SFP_thm };
   9.118 +      { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def, DEFL = DEFL_thm };
   9.119    in
   9.120      ((info, cpo_info, pcpo_info, rep_info), thy)
   9.121    end
    10.1 --- a/src/HOLCF/UpperPD.thy	Mon Oct 11 07:09:42 2010 -0700
    10.2 +++ b/src/HOLCF/UpperPD.thy	Mon Oct 11 08:32:09 2010 -0700
    10.3 @@ -447,14 +447,14 @@
    10.4      by (intro finite_deflation_upper_map finite_deflation_udom_approx)
    10.5  qed
    10.6  
    10.7 -definition upper_sfp :: "sfp \<rightarrow> sfp"
    10.8 -where "upper_sfp = sfp_fun1 upper_approx upper_map"
    10.9 +definition upper_defl :: "defl \<rightarrow> defl"
   10.10 +where "upper_defl = defl_fun1 upper_approx upper_map"
   10.11  
   10.12 -lemma cast_upper_sfp:
   10.13 -  "cast\<cdot>(upper_sfp\<cdot>A) =
   10.14 +lemma cast_upper_defl:
   10.15 +  "cast\<cdot>(upper_defl\<cdot>A) =
   10.16      udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
   10.17 -unfolding upper_sfp_def
   10.18 -apply (rule cast_sfp_fun1 [OF upper_approx])
   10.19 +unfolding upper_defl_def
   10.20 +apply (rule cast_defl_fun1 [OF upper_approx])
   10.21  apply (erule finite_deflation_upper_map)
   10.22  done
   10.23  
   10.24 @@ -468,7 +468,7 @@
   10.25    "prj = upper_map\<cdot>prj oo udom_prj upper_approx"
   10.26  
   10.27  definition
   10.28 -  "sfp (t::'a upper_pd itself) = upper_sfp\<cdot>SFP('a)"
   10.29 +  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
   10.30  
   10.31  instance proof
   10.32    show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
   10.33 @@ -476,15 +476,15 @@
   10.34      using ep_pair_udom [OF upper_approx]
   10.35      by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
   10.36  next
   10.37 -  show "cast\<cdot>SFP('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
   10.38 -    unfolding emb_upper_pd_def prj_upper_pd_def sfp_upper_pd_def cast_upper_sfp
   10.39 -    by (simp add: cast_SFP oo_def expand_cfun_eq upper_map_map)
   10.40 +  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
   10.41 +    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
   10.42 +    by (simp add: cast_DEFL oo_def expand_cfun_eq upper_map_map)
   10.43  qed
   10.44  
   10.45  end
   10.46  
   10.47 -lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
   10.48 -by (rule sfp_upper_pd_def)
   10.49 +lemma DEFL_upper: "DEFL('a upper_pd) = upper_defl\<cdot>DEFL('a)"
   10.50 +by (rule defl_upper_pd_def)
   10.51  
   10.52  
   10.53  subsection {* Join *}
    11.1 --- a/src/HOLCF/ex/Domain_Proofs.thy	Mon Oct 11 07:09:42 2010 -0700
    11.2 +++ b/src/HOLCF/ex/Domain_Proofs.thy	Mon Oct 11 08:32:09 2010 -0700
    11.3 @@ -28,50 +28,50 @@
    11.4  text {* Start with the one-step non-recursive version *}
    11.5  
    11.6  definition
    11.7 -  foo_bar_baz_sfpF ::
    11.8 -    "sfp \<rightarrow> sfp \<times> sfp \<times> sfp \<rightarrow> sfp \<times> sfp \<times> sfp"
    11.9 +  foo_bar_baz_deflF ::
   11.10 +    "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
   11.11  where
   11.12 -  "foo_bar_baz_sfpF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
   11.13 -    ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>t2))
   11.14 -    , u_sfp\<cdot>(cfun_sfp\<cdot>t3\<cdot>SFP(tr))
   11.15 -    , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>t1)\<cdot>SFP(tr)))))"
   11.16 +  "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
   11.17 +    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
   11.18 +    , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
   11.19 +    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
   11.20  
   11.21 -lemma foo_bar_baz_sfpF_beta:
   11.22 -  "foo_bar_baz_sfpF\<cdot>a\<cdot>t =
   11.23 -    ( ssum_sfp\<cdot>SFP(one)\<cdot>(sprod_sfp\<cdot>(u_sfp\<cdot>a)\<cdot>(u_sfp\<cdot>(fst (snd t))))
   11.24 -    , u_sfp\<cdot>(cfun_sfp\<cdot>(snd (snd t))\<cdot>SFP(tr))
   11.25 -    , u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(fst t))\<cdot>SFP(tr)))"
   11.26 -unfolding foo_bar_baz_sfpF_def
   11.27 +lemma foo_bar_baz_deflF_beta:
   11.28 +  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
   11.29 +    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
   11.30 +    , u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr))
   11.31 +    , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))"
   11.32 +unfolding foo_bar_baz_deflF_def
   11.33  by (simp add: split_def)
   11.34  
   11.35  text {* Individual type combinators are projected from the fixed point. *}
   11.36  
   11.37 -definition foo_sfp :: "sfp \<rightarrow> sfp"
   11.38 -where "foo_sfp = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
   11.39 +definition foo_defl :: "defl \<rightarrow> defl"
   11.40 +where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
   11.41  
   11.42 -definition bar_sfp :: "sfp \<rightarrow> sfp"
   11.43 -where "bar_sfp = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
   11.44 +definition bar_defl :: "defl \<rightarrow> defl"
   11.45 +where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
   11.46  
   11.47 -definition baz_sfp :: "sfp \<rightarrow> sfp"
   11.48 -where "baz_sfp = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))))"
   11.49 +definition baz_defl :: "defl \<rightarrow> defl"
   11.50 +where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
   11.51  
   11.52  lemma defl_apply_thms:
   11.53 -  "foo_sfp\<cdot>a = fst (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a))"
   11.54 -  "bar_sfp\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
   11.55 -  "baz_sfp\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_sfpF\<cdot>a)))"
   11.56 -unfolding foo_sfp_def bar_sfp_def baz_sfp_def by simp_all
   11.57 +  "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
   11.58 +  "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
   11.59 +  "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
   11.60 +unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
   11.61  
   11.62  text {* Unfold rules for each combinator. *}
   11.63  
   11.64 -lemma foo_sfp_unfold:
   11.65 -  "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)))"
   11.66 -unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
   11.67 +lemma foo_defl_unfold:
   11.68 +  "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)))"
   11.69 +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
   11.70  
   11.71 -lemma bar_sfp_unfold: "bar_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(baz_sfp\<cdot>a)\<cdot>SFP(tr))"
   11.72 -unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
   11.73 +lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))"
   11.74 +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
   11.75  
   11.76 -lemma baz_sfp_unfold: "baz_sfp\<cdot>a = u_sfp\<cdot>(cfun_sfp\<cdot>(convex_sfp\<cdot>(foo_sfp\<cdot>a))\<cdot>SFP(tr))"
   11.77 -unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_sfpF_beta)
   11.78 +lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>DEFL(tr))"
   11.79 +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
   11.80  
   11.81  text "The automation for the previous steps will be quite similar to
   11.82  how the fixrec package works."
   11.83 @@ -82,14 +82,14 @@
   11.84  
   11.85  text {* Use @{text pcpodef} with the appropriate type combinator. *}
   11.86  
   11.87 -pcpodef (open) 'a foo = "{x. x ::: foo_sfp\<cdot>SFP('a)}"
   11.88 -by (simp_all add: adm_in_sfp)
   11.89 +pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>DEFL('a)}"
   11.90 +by (simp_all add: adm_in_defl)
   11.91  
   11.92 -pcpodef (open) 'a bar = "{x. x ::: bar_sfp\<cdot>SFP('a)}"
   11.93 -by (simp_all add: adm_in_sfp)
   11.94 +pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>DEFL('a)}"
   11.95 +by (simp_all add: adm_in_defl)
   11.96  
   11.97 -pcpodef (open) 'a baz = "{x. x ::: baz_sfp\<cdot>SFP('a)}"
   11.98 -by (simp_all add: adm_in_sfp)
   11.99 +pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>DEFL('a)}"
  11.100 +by (simp_all add: adm_in_defl)
  11.101  
  11.102  text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
  11.103  
  11.104 @@ -100,10 +100,10 @@
  11.105  where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
  11.106  
  11.107  definition prj_foo :: "udom \<rightarrow> 'a foo"
  11.108 -where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_sfp\<cdot>SFP('a))\<cdot>y))"
  11.109 +where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
  11.110  
  11.111 -definition sfp_foo :: "'a foo itself \<Rightarrow> sfp"
  11.112 -where "sfp_foo \<equiv> \<lambda>a. foo_sfp\<cdot>SFP('a)"
  11.113 +definition defl_foo :: "'a foo itself \<Rightarrow> defl"
  11.114 +where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
  11.115  
  11.116  instance
  11.117  apply (rule typedef_rep_class)
  11.118 @@ -111,7 +111,7 @@
  11.119  apply (rule below_foo_def)
  11.120  apply (rule emb_foo_def)
  11.121  apply (rule prj_foo_def)
  11.122 -apply (rule sfp_foo_def)
  11.123 +apply (rule defl_foo_def)
  11.124  done
  11.125  
  11.126  end
  11.127 @@ -123,10 +123,10 @@
  11.128  where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
  11.129  
  11.130  definition prj_bar :: "udom \<rightarrow> 'a bar"
  11.131 -where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_sfp\<cdot>SFP('a))\<cdot>y))"
  11.132 +where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
  11.133  
  11.134 -definition sfp_bar :: "'a bar itself \<Rightarrow> sfp"
  11.135 -where "sfp_bar \<equiv> \<lambda>a. bar_sfp\<cdot>SFP('a)"
  11.136 +definition defl_bar :: "'a bar itself \<Rightarrow> defl"
  11.137 +where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
  11.138  
  11.139  instance
  11.140  apply (rule typedef_rep_class)
  11.141 @@ -134,7 +134,7 @@
  11.142  apply (rule below_bar_def)
  11.143  apply (rule emb_bar_def)
  11.144  apply (rule prj_bar_def)
  11.145 -apply (rule sfp_bar_def)
  11.146 +apply (rule defl_bar_def)
  11.147  done
  11.148  
  11.149  end
  11.150 @@ -146,10 +146,10 @@
  11.151  where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
  11.152  
  11.153  definition prj_baz :: "udom \<rightarrow> 'a baz"
  11.154 -where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_sfp\<cdot>SFP('a))\<cdot>y))"
  11.155 +where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
  11.156  
  11.157 -definition sfp_baz :: "'a baz itself \<Rightarrow> sfp"
  11.158 -where "sfp_baz \<equiv> \<lambda>a. baz_sfp\<cdot>SFP('a)"
  11.159 +definition defl_baz :: "'a baz itself \<Rightarrow> defl"
  11.160 +where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
  11.161  
  11.162  instance
  11.163  apply (rule typedef_rep_class)
  11.164 @@ -157,44 +157,44 @@
  11.165  apply (rule below_baz_def)
  11.166  apply (rule emb_baz_def)
  11.167  apply (rule prj_baz_def)
  11.168 -apply (rule sfp_baz_def)
  11.169 +apply (rule defl_baz_def)
  11.170  done
  11.171  
  11.172  end
  11.173  
  11.174 -text {* Prove SFP rules using lemma @{text typedef_SFP}. *}
  11.175 +text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
  11.176  
  11.177 -lemma SFP_foo: "SFP('a foo) = foo_sfp\<cdot>SFP('a)"
  11.178 -apply (rule typedef_SFP)
  11.179 -apply (rule sfp_foo_def)
  11.180 +lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
  11.181 +apply (rule typedef_DEFL)
  11.182 +apply (rule defl_foo_def)
  11.183  done
  11.184  
  11.185 -lemma SFP_bar: "SFP('a bar) = bar_sfp\<cdot>SFP('a)"
  11.186 -apply (rule typedef_SFP)
  11.187 -apply (rule sfp_bar_def)
  11.188 +lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
  11.189 +apply (rule typedef_DEFL)
  11.190 +apply (rule defl_bar_def)
  11.191  done
  11.192  
  11.193 -lemma SFP_baz: "SFP('a baz) = baz_sfp\<cdot>SFP('a)"
  11.194 -apply (rule typedef_SFP)
  11.195 -apply (rule sfp_baz_def)
  11.196 +lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
  11.197 +apply (rule typedef_DEFL)
  11.198 +apply (rule defl_baz_def)
  11.199  done
  11.200  
  11.201 -text {* Prove SFP equations using type combinator unfold lemmas. *}
  11.202 +text {* Prove DEFL equations using type combinator unfold lemmas. *}
  11.203  
  11.204 -lemmas SFP_simps =
  11.205 -  SFP_ssum SFP_sprod SFP_u SFP_cfun
  11.206 +lemmas DEFL_simps =
  11.207 +  DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun
  11.208  
  11.209 -lemma SFP_foo': "SFP('a foo) = SFP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
  11.210 -unfolding SFP_foo SFP_bar SFP_baz SFP_simps
  11.211 -by (rule foo_sfp_unfold)
  11.212 +lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
  11.213 +unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
  11.214 +by (rule foo_defl_unfold)
  11.215  
  11.216 -lemma SFP_bar': "SFP('a bar) = SFP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
  11.217 -unfolding SFP_foo SFP_bar SFP_baz SFP_simps
  11.218 -by (rule bar_sfp_unfold)
  11.219 +lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
  11.220 +unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps
  11.221 +by (rule bar_defl_unfold)
  11.222  
  11.223 -lemma SFP_baz': "SFP('a baz) = SFP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
  11.224 -unfolding SFP_foo SFP_bar SFP_baz SFP_simps SFP_convex
  11.225 -by (rule baz_sfp_unfold)
  11.226 +lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
  11.227 +unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps DEFL_convex
  11.228 +by (rule baz_defl_unfold)
  11.229  
  11.230  (********************************************************************)
  11.231  
  11.232 @@ -223,36 +223,36 @@
  11.233  text {* Prove isomorphism rules. *}
  11.234  
  11.235  lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
  11.236 -by (rule domain_abs_iso [OF SFP_foo' foo_abs_def foo_rep_def])
  11.237 +by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
  11.238  
  11.239  lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
  11.240 -by (rule domain_rep_iso [OF SFP_foo' foo_abs_def foo_rep_def])
  11.241 +by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
  11.242  
  11.243  lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
  11.244 -by (rule domain_abs_iso [OF SFP_bar' bar_abs_def bar_rep_def])
  11.245 +by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
  11.246  
  11.247  lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
  11.248 -by (rule domain_rep_iso [OF SFP_bar' bar_abs_def bar_rep_def])
  11.249 +by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
  11.250  
  11.251  lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
  11.252 -by (rule domain_abs_iso [OF SFP_baz' baz_abs_def baz_rep_def])
  11.253 +by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
  11.254  
  11.255  lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
  11.256 -by (rule domain_rep_iso [OF SFP_baz' baz_abs_def baz_rep_def])
  11.257 +by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
  11.258  
  11.259  text {* Prove isodefl rules using @{text isodefl_coerce}. *}
  11.260  
  11.261  lemma isodefl_foo_abs:
  11.262    "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
  11.263 -by (rule isodefl_abs_rep [OF SFP_foo' foo_abs_def foo_rep_def])
  11.264 +by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
  11.265  
  11.266  lemma isodefl_bar_abs:
  11.267    "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
  11.268 -by (rule isodefl_abs_rep [OF SFP_bar' bar_abs_def bar_rep_def])
  11.269 +by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
  11.270  
  11.271  lemma isodefl_baz_abs:
  11.272    "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
  11.273 -by (rule isodefl_abs_rep [OF SFP_baz' baz_abs_def baz_rep_def])
  11.274 +by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
  11.275  
  11.276  (********************************************************************)
  11.277  
  11.278 @@ -316,15 +316,15 @@
  11.279  lemma isodefl_foo_bar_baz:
  11.280    assumes isodefl_d: "isodefl d t"
  11.281    shows
  11.282 -  "isodefl (foo_map\<cdot>d) (foo_sfp\<cdot>t) \<and>
  11.283 -  isodefl (bar_map\<cdot>d) (bar_sfp\<cdot>t) \<and>
  11.284 -  isodefl (baz_map\<cdot>d) (baz_sfp\<cdot>t)"
  11.285 +  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
  11.286 +  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
  11.287 +  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
  11.288  unfolding map_apply_thms defl_apply_thms
  11.289   apply (rule parallel_fix_ind)
  11.290     apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
  11.291    apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
  11.292   apply (simp only: foo_bar_baz_mapF_beta
  11.293 -                   foo_bar_baz_sfpF_beta
  11.294 +                   foo_bar_baz_deflF_beta
  11.295                     fst_conv snd_conv)
  11.296   apply (elim conjE)
  11.297   apply (intro
  11.298 @@ -332,7 +332,7 @@
  11.299    isodefl_foo_abs
  11.300    isodefl_bar_abs
  11.301    isodefl_baz_abs
  11.302 -  isodefl_ssum isodefl_sprod isodefl_ID_SFP
  11.303 +  isodefl_ssum isodefl_sprod isodefl_ID_DEFL
  11.304    isodefl_u isodefl_convex isodefl_cfun
  11.305    isodefl_d
  11.306   )
  11.307 @@ -343,27 +343,27 @@
  11.308  lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
  11.309  lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
  11.310  
  11.311 -text {* Prove map ID lemmas, using isodefl_SFP_imp_ID *}
  11.312 +text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
  11.313  
  11.314  lemma foo_map_ID: "foo_map\<cdot>ID = ID"
  11.315 -apply (rule isodefl_SFP_imp_ID)
  11.316 -apply (subst SFP_foo)
  11.317 +apply (rule isodefl_DEFL_imp_ID)
  11.318 +apply (subst DEFL_foo)
  11.319  apply (rule isodefl_foo)
  11.320 -apply (rule isodefl_ID_SFP)
  11.321 +apply (rule isodefl_ID_DEFL)
  11.322  done
  11.323  
  11.324  lemma bar_map_ID: "bar_map\<cdot>ID = ID"
  11.325 -apply (rule isodefl_SFP_imp_ID)
  11.326 -apply (subst SFP_bar)
  11.327 +apply (rule isodefl_DEFL_imp_ID)
  11.328 +apply (subst DEFL_bar)
  11.329  apply (rule isodefl_bar)
  11.330 -apply (rule isodefl_ID_SFP)
  11.331 +apply (rule isodefl_ID_DEFL)
  11.332  done
  11.333  
  11.334  lemma baz_map_ID: "baz_map\<cdot>ID = ID"
  11.335 -apply (rule isodefl_SFP_imp_ID)
  11.336 -apply (subst SFP_baz)
  11.337 +apply (rule isodefl_DEFL_imp_ID)
  11.338 +apply (subst DEFL_baz)
  11.339  apply (rule isodefl_baz)
  11.340 -apply (rule isodefl_ID_SFP)
  11.341 +apply (rule isodefl_ID_DEFL)
  11.342  done
  11.343  
  11.344  (********************************************************************)