# HG changeset patch
# User huffman
# Date 1292769281 28800
# Node ID 029a6fc1bfb8f03472faf9f7f887e9a8213b6adf
# Parent  3d7685a4a5ff191aa24d6298ad49c47fbe626bc0
type 'defl' takes a type parameter again (cf. b525988432e9)

diff -r 3d7685a4a5ff -r 029a6fc1bfb8 NEWS
--- a/NEWS	Sun Dec 19 05:15:31 2010 -0800
+++ b/NEWS	Sun Dec 19 06:34:41 2010 -0800
@@ -490,9 +490,9 @@
 * The 'bifinite' class no longer fixes a constant 'approx'; the class
 now just asserts that such a function exists. INCOMPATIBILITY.
 
-* The type 'udom alg_defl' has been replaced by the non-parameterized
-type 'defl'. HOLCF no longer defines an embedding of type defl into
-udom by default; the instance proof defl :: domain is now available in
+* The type 'alg_defl' has been renamed to 'defl'. HOLCF no longer
+defines an embedding of type 'a defl into udom by default; instances
+of 'bifinite' and 'domain' classes are available in
 HOLCF/Library/Defl_Bifinite.thy.
 
 * The syntax 'REP('a)' has been replaced with 'DEFL('a)'.
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -8,21 +8,23 @@
 imports Universal Map_Functions
 begin
 
+default_sort bifinite
+
 subsection {* Type constructor for finite deflations *}
 
-typedef (open) fin_defl = "{d::udom \<rightarrow> udom. finite_deflation d}"
+typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
 by (fast intro: finite_deflation_UU)
 
-instantiation fin_defl :: below
+instantiation fin_defl :: (bifinite) below
 begin
 
 definition below_fin_defl_def:
-    "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
+  "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
 
 instance ..
 end
 
-instance fin_defl :: po
+instance fin_defl :: (bifinite) po
 using type_definition_fin_defl below_fin_defl_def
 by (rule typedef_po)
 
@@ -72,10 +74,10 @@
 
 subsection {* Defining algebraic deflations by ideal completion *}
 
-typedef (open) defl = "{S::fin_defl set. below.ideal S}"
+typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
 by (rule below.ex_ideal)
 
-instantiation defl :: below
+instantiation defl :: (bifinite) below
 begin
 
 definition
@@ -84,21 +86,21 @@
 instance ..
 end
 
-instance defl :: po
+instance defl :: (bifinite) po
 using type_definition_defl below_defl_def
 by (rule below.typedef_ideal_po)
 
-instance defl :: cpo
+instance defl :: (bifinite) cpo
 using type_definition_defl below_defl_def
 by (rule below.typedef_ideal_cpo)
 
 definition
-  defl_principal :: "fin_defl \<Rightarrow> defl" where
+  defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
   "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
 
-lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
+lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
 proof -
-  obtain f :: "udom compact_basis \<Rightarrow> nat" where inj_f: "inj f"
+  obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
     using compact_basis.countable ..
   have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
     apply (rule finite_imageI)
@@ -139,7 +141,7 @@
 apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
 done
 
-instance defl :: pcpo
+instance defl :: (bifinite) pcpo
 by intro_classes (fast intro: defl_minimal)
 
 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
@@ -148,7 +150,7 @@
 subsection {* Applying algebraic deflations *}
 
 definition
-  cast :: "defl \<rightarrow> udom \<rightarrow> udom"
+  cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
 where
   "cast = defl.basis_fun Rep_fin_defl"
 
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -490,7 +490,7 @@
 using convex_map_ID finite_deflation_convex_map
 unfolding convex_approx_def by (rule approx_chain_lemma1)
 
-definition convex_defl :: "defl \<rightarrow> defl"
+definition convex_defl :: "udom defl \<rightarrow> udom defl"
 where "convex_defl = defl_fun1 convex_approx convex_map"
 
 lemma cast_convex_defl:
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/Domain.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -63,7 +63,7 @@
 
 subsection {* Deflations as sets *}
 
-definition defl_set :: "defl \<Rightarrow> udom set"
+definition defl_set :: "'a::bifinite defl \<Rightarrow> 'a set"
 where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
 
 lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
@@ -86,10 +86,10 @@
 
 setup {*
   fold Sign.add_const_constraint
-  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
   , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
   , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
-  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
   , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
 *}
@@ -97,7 +97,7 @@
 lemma typedef_liftdomain_class:
   fixes Rep :: "'a::pcpo \<Rightarrow> udom"
   fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
-  fixes t :: defl
+  fixes t :: "udom defl"
   assumes type: "type_definition Rep Abs (defl_set t)"
   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
@@ -105,7 +105,7 @@
   assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
   assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
   assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
-  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
+  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
   shows "OFCLASS('a, liftdomain_class)"
 using liftemb [THEN meta_eq_to_obj_eq]
 using liftprj [THEN meta_eq_to_obj_eq]
@@ -148,10 +148,10 @@
 
 setup {*
   fold Sign.add_const_constraint
-  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
+  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
   , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
   , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
-  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
+  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom defl"})
   , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
 *}
@@ -161,7 +161,7 @@
 subsection {* Isomorphic deflations *}
 
 definition
-  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
+  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
 where
   "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
 
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -438,17 +438,20 @@
 
 subsection {* Take function for finite deflations *}
 
+context bifinite_approx_chain
+begin
+
 definition
-  defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
+  defl_take :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> ('a \<rightarrow> 'a)"
 where
-  "defl_take i d = eventual_iterate (udom_approx i oo d)"
+  "defl_take i d = eventual_iterate (approx i oo d)"
 
 lemma finite_deflation_defl_take:
   "deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
 unfolding defl_take_def
 apply (rule pre_deflation.finite_deflation_d)
 apply (rule pre_deflation_oo)
-apply (rule finite_deflation_udom_approx)
+apply (rule finite_deflation_approx)
 apply (erule deflation.below)
 done
 
@@ -459,10 +462,10 @@
 done
 
 lemma defl_take_fixed_iff:
-  "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
+  "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> d\<cdot>x = x"
 unfolding defl_take_def
 apply (rule eventual_iterate_oo_fixed_iff)
-apply (rule finite_deflation_udom_approx)
+apply (rule finite_deflation_approx)
 apply (erule deflation.below)
 done
 
@@ -479,11 +482,11 @@
   assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
   shows "cont (\<lambda>x. defl_take i (f x))"
 unfolding defl_take_def
-using finite_deflation_udom_approx assms
+using finite_deflation_approx assms
 by (rule cont2cont_eventual_iterate_oo)
 
 definition
-  fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
+  fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
 where
   "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
 
@@ -497,7 +500,7 @@
 
 lemma fd_take_fixed_iff:
   "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
-    udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
+    approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
 unfolding Rep_fin_defl_fd_take
 apply (rule defl_take_fixed_iff)
 apply (rule deflation_Rep_fin_defl)
@@ -519,11 +522,11 @@
 apply (simp add: fin_defl_belowD)
 done
 
-lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
+lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
 apply (rule deflation.belowD)
 apply (rule finite_deflation_imp_deflation)
-apply (rule finite_deflation_udom_approx)
-apply (erule chain_mono [OF chain_udom_approx])
+apply (rule finite_deflation_approx)
+apply (erule chain_mono [OF chain_approx])
 apply assumption
 done
 
@@ -535,16 +538,16 @@
 
 lemma finite_range_fd_take: "finite (range (fd_take n))"
 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
-apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
+apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"])
 apply (clarify, simp add: fd_take_fixed_iff)
-apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
+apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_approx])
 apply (rule inj_onI, clarify)
 apply (simp add: set_eq_iff fin_defl_eqI)
 done
 
 lemma fd_take_covers: "\<exists>n. fd_take n a = a"
 apply (rule_tac x=
-  "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
+  "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
 apply (rule below_antisym)
 apply (rule fd_take_below)
 apply (rule fin_defl_belowI)
@@ -556,7 +559,7 @@
 apply (rule imageI)
 apply (erule CollectI)
 apply (rule LeastI_ex)
-apply (rule approx_chain.compact_eq_approx [OF udom_approx])
+apply (rule compact_eq_approx)
 apply (erule subst)
 apply (rule Rep_fin_defl.compact)
 done
@@ -564,7 +567,7 @@
 subsection {* Chain of approx functions on algebraic deflations *}
 
 definition
-  defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
+  defl_approx :: "nat \<Rightarrow> 'a defl \<rightarrow> 'a defl"
 where
   "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
 
@@ -607,12 +610,34 @@
     done
 qed
 
+end
+
 subsection {* Algebraic deflations are a bifinite domain *}
 
-instance defl :: bifinite
-  by default (fast intro!: defl_approx)
+instance defl :: (bifinite) bifinite
+proof
+  obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a"
+    using bifinite ..
+  hence "bifinite_approx_chain a"
+    unfolding bifinite_approx_chain_def .
+  thus "\<exists>(a::nat \<Rightarrow> 'a defl \<rightarrow> 'a defl). approx_chain a"
+    by (fast intro: bifinite_approx_chain.defl_approx)
+qed
+
+subsection {* Algebraic deflations are representable *}
 
-instantiation defl :: liftdomain
+definition defl_approx :: "nat \<Rightarrow> 'a::bifinite defl \<rightarrow> 'a defl"
+  where "defl_approx = bifinite_approx_chain.defl_approx
+    (SOME a. approx_chain a)"
+
+lemma defl_approx: "approx_chain defl_approx"
+unfolding defl_approx_def
+apply (rule bifinite_approx_chain.defl_approx)
+apply (unfold bifinite_approx_chain_def)
+apply (rule someI_ex [OF bifinite])
+done
+
+instantiation defl :: (bifinite) liftdomain
 begin
 
 definition
@@ -622,25 +647,25 @@
   "prj = udom_prj defl_approx"
 
 definition
-  "defl (t::defl itself) =
+  "defl (t::'a defl itself) =
     (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
 
 definition
-  "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
+  "(liftemb :: 'a defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
 
 definition
-  "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
+  "(liftprj :: udom \<rightarrow> 'a defl u) = u_map\<cdot>prj oo udom_prj u_approx"
 
 definition
-  "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
+  "liftdefl (t::'a defl itself) = u_defl\<cdot>DEFL('a defl)"
 
 instance
 using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
 proof (rule liftdomain_class_intro)
-  show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
+  show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
     unfolding emb_defl_def prj_defl_def
     by (rule ep_pair_udom [OF defl_approx])
-  show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
+  show "cast\<cdot>DEFL('a defl) = emb oo (prj :: udom \<rightarrow> 'a defl)"
     unfolding defl_defl_def
     apply (subst contlub_cfun_arg)
     apply (rule chainI)
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -482,7 +482,7 @@
 using lower_map_ID finite_deflation_lower_map
 unfolding lower_approx_def by (rule approx_chain_lemma1)
 
-definition lower_defl :: "defl \<rightarrow> defl"
+definition lower_defl :: "udom defl \<rightarrow> udom defl"
 where "lower_defl = defl_fun1 lower_approx lower_map"
 
 lemma cast_lower_defl:
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -19,7 +19,7 @@
 *}
 
 class predomain = cpo +
-  fixes liftdefl :: "('a::cpo) itself \<Rightarrow> defl"
+  fixes liftdefl :: "('a::cpo) itself \<Rightarrow> udom defl"
   fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom"
   fixes liftprj :: "udom \<rightarrow> 'a\<^sub>\<bottom>"
   assumes predomain_ep: "ep_pair liftemb liftprj"
@@ -31,11 +31,11 @@
 class "domain" = predomain + pcpo +
   fixes emb :: "'a::cpo \<rightarrow> udom"
   fixes prj :: "udom \<rightarrow> 'a::cpo"
-  fixes defl :: "'a itself \<Rightarrow> defl"
+  fixes defl :: "'a itself \<Rightarrow> udom defl"
   assumes ep_pair_emb_prj: "ep_pair emb prj"
   assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
 
-syntax "_DEFL" :: "type \<Rightarrow> defl"  ("(1DEFL/(1'(_')))")
+syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
 
 interpretation "domain": pcpo_ep_pair emb prj
@@ -51,9 +51,9 @@
 subsection {* Domains are bifinite *}
 
 lemma approx_chain_ep_cast:
-  assumes ep: "ep_pair (e::'a \<rightarrow> udom) (p::udom \<rightarrow> 'a)"
+  assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> udom) (p::udom \<rightarrow> 'a)"
   assumes cast_t: "cast\<cdot>t = e oo p"
-  shows "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
+  shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a"
 proof -
   interpret ep_pair e p by fact
   obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
@@ -144,7 +144,7 @@
 
 definition
   defl_fun1 ::
-    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
+    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (udom defl \<rightarrow> udom defl)"
 where
   "defl_fun1 approx f =
     defl.basis_fun (\<lambda>a.
@@ -154,7 +154,7 @@
 definition
   defl_fun2 ::
     "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
-      \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)"
+      \<Rightarrow> (udom defl \<rightarrow> udom defl \<rightarrow> udom defl)"
 where
   "defl_fun2 approx f =
     defl.basis_fun (\<lambda>a.
@@ -213,19 +213,19 @@
                    Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
 qed
 
-definition u_defl :: "defl \<rightarrow> defl"
+definition u_defl :: "udom defl \<rightarrow> udom defl"
   where "u_defl = defl_fun1 u_approx u_map"
 
-definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   where "sfun_defl = defl_fun2 sfun_approx sfun_map"
 
-definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   where "prod_defl = defl_fun2 prod_approx cprod_map"
 
-definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
   where "sprod_defl = defl_fun2 sprod_approx sprod_map"
 
-definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
+definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
 where "ssum_defl = defl_fun2 ssum_approx ssum_map"
 
 lemma cast_u_defl:
@@ -276,10 +276,10 @@
 
 setup {*
   fold Sign.add_const_constraint
-  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
   , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
   , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
-  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
+  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
   , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
 *}
@@ -307,10 +307,10 @@
 
 setup {*
   fold Sign.add_const_constraint
-  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
+  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
   , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
   , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
-  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
+  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom defl"})
   , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
 *}
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Dec 19 06:34:41 2010 -0800
@@ -68,7 +68,7 @@
 infixr -->>
 
 val udomT = @{typ udom}
-val deflT = @{typ "defl"}
+val deflT = @{typ "udom defl"}
 
 fun mk_DEFL T =
   Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 06:34:41 2010 -0800
@@ -49,7 +49,7 @@
 (* building types and terms *)
 
 val udomT = @{typ udom}
-val deflT = @{typ defl}
+val deflT = @{typ "udom defl"}
 fun emb_const T = Const (@{const_name emb}, T ->> udomT)
 fun prj_const T = Const (@{const_name prj}, udomT ->> T)
 fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT)
@@ -68,7 +68,7 @@
 
 fun mk_cast (t, x) =
   capply_const (udomT, udomT)
-  $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
+  $ (capply_const (deflT, udomT ->> udomT) $ @{term "cast :: udom defl -> udom -> udom"} $ t)
   $ x
 
 (* manipulating theorems *)
@@ -98,7 +98,7 @@
     val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl
 
     val deflT = Term.fastype_of defl
-    val _ = if deflT = @{typ "defl"} then ()
+    val _ = if deflT = @{typ "udom defl"} then ()
             else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT))
 
     (*lhs*)
@@ -112,7 +112,7 @@
       |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
 
     (*set*)
-    val set = @{const defl_set} $ defl
+    val set = @{term "defl_set :: udom defl => udom => bool"} $ defl
 
     (*pcpodef*)
     val tac1 = rtac @{thm defl_set_bottom} 1
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -477,7 +477,7 @@
 using upper_map_ID finite_deflation_upper_map
 unfolding upper_approx_def by (rule approx_chain_lemma1)
 
-definition upper_defl :: "defl \<rightarrow> defl"
+definition upper_defl :: "udom defl \<rightarrow> udom defl"
 where "upper_defl = defl_fun1 upper_approx upper_map"
 
 lemma cast_upper_defl:
diff -r 3d7685a4a5ff -r 029a6fc1bfb8 src/HOL/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -30,7 +30,7 @@
 
 definition
   foo_bar_baz_deflF ::
-    "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
+    "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
 where
   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
@@ -47,13 +47,13 @@
 
 text {* Individual type combinators are projected from the fixed point. *}
 
-definition foo_defl :: "defl \<rightarrow> defl"
+definition foo_defl :: "udom defl \<rightarrow> udom defl"
 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
 
-definition bar_defl :: "defl \<rightarrow> defl"
+definition bar_defl :: "udom defl \<rightarrow> udom defl"
 where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
-definition baz_defl :: "defl \<rightarrow> defl"
+definition baz_defl :: "udom defl \<rightarrow> udom defl"
 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
 lemma defl_apply_thms:
@@ -103,7 +103,7 @@
 definition prj_foo :: "udom \<rightarrow> 'a foo"
 where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
-definition defl_foo :: "'a foo itself \<Rightarrow> defl"
+definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
 
 definition
@@ -138,7 +138,7 @@
 definition prj_bar :: "udom \<rightarrow> 'a bar"
 where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
-definition defl_bar :: "'a bar itself \<Rightarrow> defl"
+definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
 
 definition
@@ -173,7 +173,7 @@
 definition prj_baz :: "udom \<rightarrow> 'a baz"
 where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
-definition defl_baz :: "'a baz itself \<Rightarrow> defl"
+definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
 
 definition