type 'defl' takes a type parameter again (cf. b525988432e9)
authorhuffman
Sun Dec 19 06:34:41 2010 -0800 (2010-12-19)
changeset 41287029a6fc1bfb8
parent 41286 3d7685a4a5ff
child 41288 a19edebad961
type 'defl' takes a type parameter again (cf. b525988432e9)
NEWS
src/HOL/HOLCF/Algebraic.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/UpperPD.thy
src/HOL/HOLCF/ex/Domain_Proofs.thy
     1.1 --- a/NEWS	Sun Dec 19 05:15:31 2010 -0800
     1.2 +++ b/NEWS	Sun Dec 19 06:34:41 2010 -0800
     1.3 @@ -490,9 +490,9 @@
     1.4  * The 'bifinite' class no longer fixes a constant 'approx'; the class
     1.5  now just asserts that such a function exists. INCOMPATIBILITY.
     1.6  
     1.7 -* The type 'udom alg_defl' has been replaced by the non-parameterized
     1.8 -type 'defl'. HOLCF no longer defines an embedding of type defl into
     1.9 -udom by default; the instance proof defl :: domain is now available in
    1.10 +* The type 'alg_defl' has been renamed to 'defl'. HOLCF no longer
    1.11 +defines an embedding of type 'a defl into udom by default; instances
    1.12 +of 'bifinite' and 'domain' classes are available in
    1.13  HOLCF/Library/Defl_Bifinite.thy.
    1.14  
    1.15  * The syntax 'REP('a)' has been replaced with 'DEFL('a)'.
     2.1 --- a/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 05:15:31 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 06:34:41 2010 -0800
     2.3 @@ -8,21 +8,23 @@
     2.4  imports Universal Map_Functions
     2.5  begin
     2.6  
     2.7 +default_sort bifinite
     2.8 +
     2.9  subsection {* Type constructor for finite deflations *}
    2.10  
    2.11 -typedef (open) fin_defl = "{d::udom \<rightarrow> udom. finite_deflation d}"
    2.12 +typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
    2.13  by (fast intro: finite_deflation_UU)
    2.14  
    2.15 -instantiation fin_defl :: below
    2.16 +instantiation fin_defl :: (bifinite) below
    2.17  begin
    2.18  
    2.19  definition below_fin_defl_def:
    2.20 -    "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
    2.21 +  "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
    2.22  
    2.23  instance ..
    2.24  end
    2.25  
    2.26 -instance fin_defl :: po
    2.27 +instance fin_defl :: (bifinite) po
    2.28  using type_definition_fin_defl below_fin_defl_def
    2.29  by (rule typedef_po)
    2.30  
    2.31 @@ -72,10 +74,10 @@
    2.32  
    2.33  subsection {* Defining algebraic deflations by ideal completion *}
    2.34  
    2.35 -typedef (open) defl = "{S::fin_defl set. below.ideal S}"
    2.36 +typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
    2.37  by (rule below.ex_ideal)
    2.38  
    2.39 -instantiation defl :: below
    2.40 +instantiation defl :: (bifinite) below
    2.41  begin
    2.42  
    2.43  definition
    2.44 @@ -84,21 +86,21 @@
    2.45  instance ..
    2.46  end
    2.47  
    2.48 -instance defl :: po
    2.49 +instance defl :: (bifinite) po
    2.50  using type_definition_defl below_defl_def
    2.51  by (rule below.typedef_ideal_po)
    2.52  
    2.53 -instance defl :: cpo
    2.54 +instance defl :: (bifinite) cpo
    2.55  using type_definition_defl below_defl_def
    2.56  by (rule below.typedef_ideal_cpo)
    2.57  
    2.58  definition
    2.59 -  defl_principal :: "fin_defl \<Rightarrow> defl" where
    2.60 +  defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
    2.61    "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
    2.62  
    2.63 -lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
    2.64 +lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
    2.65  proof -
    2.66 -  obtain f :: "udom compact_basis \<Rightarrow> nat" where inj_f: "inj f"
    2.67 +  obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
    2.68      using compact_basis.countable ..
    2.69    have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
    2.70      apply (rule finite_imageI)
    2.71 @@ -139,7 +141,7 @@
    2.72  apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
    2.73  done
    2.74  
    2.75 -instance defl :: pcpo
    2.76 +instance defl :: (bifinite) pcpo
    2.77  by intro_classes (fast intro: defl_minimal)
    2.78  
    2.79  lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
    2.80 @@ -148,7 +150,7 @@
    2.81  subsection {* Applying algebraic deflations *}
    2.82  
    2.83  definition
    2.84 -  cast :: "defl \<rightarrow> udom \<rightarrow> udom"
    2.85 +  cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
    2.86  where
    2.87    "cast = defl.basis_fun Rep_fin_defl"
    2.88  
     3.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 05:15:31 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:34:41 2010 -0800
     3.3 @@ -490,7 +490,7 @@
     3.4  using convex_map_ID finite_deflation_convex_map
     3.5  unfolding convex_approx_def by (rule approx_chain_lemma1)
     3.6  
     3.7 -definition convex_defl :: "defl \<rightarrow> defl"
     3.8 +definition convex_defl :: "udom defl \<rightarrow> udom defl"
     3.9  where "convex_defl = defl_fun1 convex_approx convex_map"
    3.10  
    3.11  lemma cast_convex_defl:
     4.1 --- a/src/HOL/HOLCF/Domain.thy	Sun Dec 19 05:15:31 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Domain.thy	Sun Dec 19 06:34:41 2010 -0800
     4.3 @@ -63,7 +63,7 @@
     4.4  
     4.5  subsection {* Deflations as sets *}
     4.6  
     4.7 -definition defl_set :: "defl \<Rightarrow> udom set"
     4.8 +definition defl_set :: "'a::bifinite defl \<Rightarrow> 'a set"
     4.9  where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
    4.10  
    4.11  lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
    4.12 @@ -86,10 +86,10 @@
    4.13  
    4.14  setup {*
    4.15    fold Sign.add_const_constraint
    4.16 -  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
    4.17 +  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
    4.18    , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
    4.19    , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
    4.20 -  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
    4.21 +  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
    4.22    , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
    4.23    , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
    4.24  *}
    4.25 @@ -97,7 +97,7 @@
    4.26  lemma typedef_liftdomain_class:
    4.27    fixes Rep :: "'a::pcpo \<Rightarrow> udom"
    4.28    fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
    4.29 -  fixes t :: defl
    4.30 +  fixes t :: "udom defl"
    4.31    assumes type: "type_definition Rep Abs (defl_set t)"
    4.32    assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    4.33    assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
    4.34 @@ -105,7 +105,7 @@
    4.35    assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
    4.36    assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
    4.37    assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
    4.38 -  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
    4.39 +  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> _) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
    4.40    shows "OFCLASS('a, liftdomain_class)"
    4.41  using liftemb [THEN meta_eq_to_obj_eq]
    4.42  using liftprj [THEN meta_eq_to_obj_eq]
    4.43 @@ -148,10 +148,10 @@
    4.44  
    4.45  setup {*
    4.46    fold Sign.add_const_constraint
    4.47 -  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
    4.48 +  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
    4.49    , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
    4.50    , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
    4.51 -  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
    4.52 +  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom defl"})
    4.53    , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
    4.54    , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
    4.55  *}
    4.56 @@ -161,7 +161,7 @@
    4.57  subsection {* Isomorphic deflations *}
    4.58  
    4.59  definition
    4.60 -  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
    4.61 +  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
    4.62  where
    4.63    "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
    4.64  
     5.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 06:34:41 2010 -0800
     5.3 @@ -438,17 +438,20 @@
     5.4  
     5.5  subsection {* Take function for finite deflations *}
     5.6  
     5.7 +context bifinite_approx_chain
     5.8 +begin
     5.9 +
    5.10  definition
    5.11 -  defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)"
    5.12 +  defl_take :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> ('a \<rightarrow> 'a)"
    5.13  where
    5.14 -  "defl_take i d = eventual_iterate (udom_approx i oo d)"
    5.15 +  "defl_take i d = eventual_iterate (approx i oo d)"
    5.16  
    5.17  lemma finite_deflation_defl_take:
    5.18    "deflation d \<Longrightarrow> finite_deflation (defl_take i d)"
    5.19  unfolding defl_take_def
    5.20  apply (rule pre_deflation.finite_deflation_d)
    5.21  apply (rule pre_deflation_oo)
    5.22 -apply (rule finite_deflation_udom_approx)
    5.23 +apply (rule finite_deflation_approx)
    5.24  apply (erule deflation.below)
    5.25  done
    5.26  
    5.27 @@ -459,10 +462,10 @@
    5.28  done
    5.29  
    5.30  lemma defl_take_fixed_iff:
    5.31 -  "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x"
    5.32 +  "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> d\<cdot>x = x"
    5.33  unfolding defl_take_def
    5.34  apply (rule eventual_iterate_oo_fixed_iff)
    5.35 -apply (rule finite_deflation_udom_approx)
    5.36 +apply (rule finite_deflation_approx)
    5.37  apply (erule deflation.below)
    5.38  done
    5.39  
    5.40 @@ -479,11 +482,11 @@
    5.41    assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
    5.42    shows "cont (\<lambda>x. defl_take i (f x))"
    5.43  unfolding defl_take_def
    5.44 -using finite_deflation_udom_approx assms
    5.45 +using finite_deflation_approx assms
    5.46  by (rule cont2cont_eventual_iterate_oo)
    5.47  
    5.48  definition
    5.49 -  fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl"
    5.50 +  fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
    5.51  where
    5.52    "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))"
    5.53  
    5.54 @@ -497,7 +500,7 @@
    5.55  
    5.56  lemma fd_take_fixed_iff:
    5.57    "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
    5.58 -    udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
    5.59 +    approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
    5.60  unfolding Rep_fin_defl_fd_take
    5.61  apply (rule defl_take_fixed_iff)
    5.62  apply (rule deflation_Rep_fin_defl)
    5.63 @@ -519,11 +522,11 @@
    5.64  apply (simp add: fin_defl_belowD)
    5.65  done
    5.66  
    5.67 -lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x"
    5.68 +lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
    5.69  apply (rule deflation.belowD)
    5.70  apply (rule finite_deflation_imp_deflation)
    5.71 -apply (rule finite_deflation_udom_approx)
    5.72 -apply (erule chain_mono [OF chain_udom_approx])
    5.73 +apply (rule finite_deflation_approx)
    5.74 +apply (erule chain_mono [OF chain_approx])
    5.75  apply assumption
    5.76  done
    5.77  
    5.78 @@ -535,16 +538,16 @@
    5.79  
    5.80  lemma finite_range_fd_take: "finite (range (fd_take n))"
    5.81  apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
    5.82 -apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"])
    5.83 +apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"])
    5.84  apply (clarify, simp add: fd_take_fixed_iff)
    5.85 -apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx])
    5.86 +apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_approx])
    5.87  apply (rule inj_onI, clarify)
    5.88  apply (simp add: set_eq_iff fin_defl_eqI)
    5.89  done
    5.90  
    5.91  lemma fd_take_covers: "\<exists>n. fd_take n a = a"
    5.92  apply (rule_tac x=
    5.93 -  "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
    5.94 +  "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
    5.95  apply (rule below_antisym)
    5.96  apply (rule fd_take_below)
    5.97  apply (rule fin_defl_belowI)
    5.98 @@ -556,7 +559,7 @@
    5.99  apply (rule imageI)
   5.100  apply (erule CollectI)
   5.101  apply (rule LeastI_ex)
   5.102 -apply (rule approx_chain.compact_eq_approx [OF udom_approx])
   5.103 +apply (rule compact_eq_approx)
   5.104  apply (erule subst)
   5.105  apply (rule Rep_fin_defl.compact)
   5.106  done
   5.107 @@ -564,7 +567,7 @@
   5.108  subsection {* Chain of approx functions on algebraic deflations *}
   5.109  
   5.110  definition
   5.111 -  defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl"
   5.112 +  defl_approx :: "nat \<Rightarrow> 'a defl \<rightarrow> 'a defl"
   5.113  where
   5.114    "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
   5.115  
   5.116 @@ -607,12 +610,34 @@
   5.117      done
   5.118  qed
   5.119  
   5.120 +end
   5.121 +
   5.122  subsection {* Algebraic deflations are a bifinite domain *}
   5.123  
   5.124 -instance defl :: bifinite
   5.125 -  by default (fast intro!: defl_approx)
   5.126 +instance defl :: (bifinite) bifinite
   5.127 +proof
   5.128 +  obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a"
   5.129 +    using bifinite ..
   5.130 +  hence "bifinite_approx_chain a"
   5.131 +    unfolding bifinite_approx_chain_def .
   5.132 +  thus "\<exists>(a::nat \<Rightarrow> 'a defl \<rightarrow> 'a defl). approx_chain a"
   5.133 +    by (fast intro: bifinite_approx_chain.defl_approx)
   5.134 +qed
   5.135 +
   5.136 +subsection {* Algebraic deflations are representable *}
   5.137  
   5.138 -instantiation defl :: liftdomain
   5.139 +definition defl_approx :: "nat \<Rightarrow> 'a::bifinite defl \<rightarrow> 'a defl"
   5.140 +  where "defl_approx = bifinite_approx_chain.defl_approx
   5.141 +    (SOME a. approx_chain a)"
   5.142 +
   5.143 +lemma defl_approx: "approx_chain defl_approx"
   5.144 +unfolding defl_approx_def
   5.145 +apply (rule bifinite_approx_chain.defl_approx)
   5.146 +apply (unfold bifinite_approx_chain_def)
   5.147 +apply (rule someI_ex [OF bifinite])
   5.148 +done
   5.149 +
   5.150 +instantiation defl :: (bifinite) liftdomain
   5.151  begin
   5.152  
   5.153  definition
   5.154 @@ -622,25 +647,25 @@
   5.155    "prj = udom_prj defl_approx"
   5.156  
   5.157  definition
   5.158 -  "defl (t::defl itself) =
   5.159 +  "defl (t::'a defl itself) =
   5.160      (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))"
   5.161  
   5.162  definition
   5.163 -  "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.164 +  "(liftemb :: 'a defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   5.165  
   5.166  definition
   5.167 -  "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.168 +  "(liftprj :: udom \<rightarrow> 'a defl u) = u_map\<cdot>prj oo udom_prj u_approx"
   5.169  
   5.170  definition
   5.171 -  "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)"
   5.172 +  "liftdefl (t::'a defl itself) = u_defl\<cdot>DEFL('a defl)"
   5.173  
   5.174  instance
   5.175  using liftemb_defl_def liftprj_defl_def liftdefl_defl_def
   5.176  proof (rule liftdomain_class_intro)
   5.177 -  show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)"
   5.178 +  show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)"
   5.179      unfolding emb_defl_def prj_defl_def
   5.180      by (rule ep_pair_udom [OF defl_approx])
   5.181 -  show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)"
   5.182 +  show "cast\<cdot>DEFL('a defl) = emb oo (prj :: udom \<rightarrow> 'a defl)"
   5.183      unfolding defl_defl_def
   5.184      apply (subst contlub_cfun_arg)
   5.185      apply (rule chainI)
     6.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 05:15:31 2010 -0800
     6.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:34:41 2010 -0800
     6.3 @@ -482,7 +482,7 @@
     6.4  using lower_map_ID finite_deflation_lower_map
     6.5  unfolding lower_approx_def by (rule approx_chain_lemma1)
     6.6  
     6.7 -definition lower_defl :: "defl \<rightarrow> defl"
     6.8 +definition lower_defl :: "udom defl \<rightarrow> udom defl"
     6.9  where "lower_defl = defl_fun1 lower_approx lower_map"
    6.10  
    6.11  lemma cast_lower_defl:
     7.1 --- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 05:15:31 2010 -0800
     7.2 +++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 06:34:41 2010 -0800
     7.3 @@ -19,7 +19,7 @@
     7.4  *}
     7.5  
     7.6  class predomain = cpo +
     7.7 -  fixes liftdefl :: "('a::cpo) itself \<Rightarrow> defl"
     7.8 +  fixes liftdefl :: "('a::cpo) itself \<Rightarrow> udom defl"
     7.9    fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom"
    7.10    fixes liftprj :: "udom \<rightarrow> 'a\<^sub>\<bottom>"
    7.11    assumes predomain_ep: "ep_pair liftemb liftprj"
    7.12 @@ -31,11 +31,11 @@
    7.13  class "domain" = predomain + pcpo +
    7.14    fixes emb :: "'a::cpo \<rightarrow> udom"
    7.15    fixes prj :: "udom \<rightarrow> 'a::cpo"
    7.16 -  fixes defl :: "'a itself \<Rightarrow> defl"
    7.17 +  fixes defl :: "'a itself \<Rightarrow> udom defl"
    7.18    assumes ep_pair_emb_prj: "ep_pair emb prj"
    7.19    assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
    7.20  
    7.21 -syntax "_DEFL" :: "type \<Rightarrow> defl"  ("(1DEFL/(1'(_')))")
    7.22 +syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
    7.23  translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
    7.24  
    7.25  interpretation "domain": pcpo_ep_pair emb prj
    7.26 @@ -51,9 +51,9 @@
    7.27  subsection {* Domains are bifinite *}
    7.28  
    7.29  lemma approx_chain_ep_cast:
    7.30 -  assumes ep: "ep_pair (e::'a \<rightarrow> udom) (p::udom \<rightarrow> 'a)"
    7.31 +  assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> udom) (p::udom \<rightarrow> 'a)"
    7.32    assumes cast_t: "cast\<cdot>t = e oo p"
    7.33 -  shows "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
    7.34 +  shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a"
    7.35  proof -
    7.36    interpret ep_pair e p by fact
    7.37    obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
    7.38 @@ -144,7 +144,7 @@
    7.39  
    7.40  definition
    7.41    defl_fun1 ::
    7.42 -    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
    7.43 +    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (udom defl \<rightarrow> udom defl)"
    7.44  where
    7.45    "defl_fun1 approx f =
    7.46      defl.basis_fun (\<lambda>a.
    7.47 @@ -154,7 +154,7 @@
    7.48  definition
    7.49    defl_fun2 ::
    7.50      "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
    7.51 -      \<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)"
    7.52 +      \<Rightarrow> (udom defl \<rightarrow> udom defl \<rightarrow> udom defl)"
    7.53  where
    7.54    "defl_fun2 approx f =
    7.55      defl.basis_fun (\<lambda>a.
    7.56 @@ -213,19 +213,19 @@
    7.57                     Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
    7.58  qed
    7.59  
    7.60 -definition u_defl :: "defl \<rightarrow> defl"
    7.61 +definition u_defl :: "udom defl \<rightarrow> udom defl"
    7.62    where "u_defl = defl_fun1 u_approx u_map"
    7.63  
    7.64 -definition sfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    7.65 +definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    7.66    where "sfun_defl = defl_fun2 sfun_approx sfun_map"
    7.67  
    7.68 -definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    7.69 +definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    7.70    where "prod_defl = defl_fun2 prod_approx cprod_map"
    7.71  
    7.72 -definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    7.73 +definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    7.74    where "sprod_defl = defl_fun2 sprod_approx sprod_map"
    7.75  
    7.76 -definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    7.77 +definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
    7.78  where "ssum_defl = defl_fun2 ssum_approx ssum_map"
    7.79  
    7.80  lemma cast_u_defl:
    7.81 @@ -276,10 +276,10 @@
    7.82  
    7.83  setup {*
    7.84    fold Sign.add_const_constraint
    7.85 -  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
    7.86 +  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
    7.87    , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
    7.88    , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
    7.89 -  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
    7.90 +  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
    7.91    , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
    7.92    , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
    7.93  *}
    7.94 @@ -307,10 +307,10 @@
    7.95  
    7.96  setup {*
    7.97    fold Sign.add_const_constraint
    7.98 -  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
    7.99 +  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
   7.100    , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
   7.101    , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
   7.102 -  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
   7.103 +  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom defl"})
   7.104    , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
   7.105    , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
   7.106  *}
     8.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Dec 19 05:15:31 2010 -0800
     8.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Dec 19 06:34:41 2010 -0800
     8.3 @@ -68,7 +68,7 @@
     8.4  infixr -->>
     8.5  
     8.6  val udomT = @{typ udom}
     8.7 -val deflT = @{typ "defl"}
     8.8 +val deflT = @{typ "udom defl"}
     8.9  
    8.10  fun mk_DEFL T =
    8.11    Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T
     9.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 05:15:31 2010 -0800
     9.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 06:34:41 2010 -0800
     9.3 @@ -49,7 +49,7 @@
     9.4  (* building types and terms *)
     9.5  
     9.6  val udomT = @{typ udom}
     9.7 -val deflT = @{typ defl}
     9.8 +val deflT = @{typ "udom defl"}
     9.9  fun emb_const T = Const (@{const_name emb}, T ->> udomT)
    9.10  fun prj_const T = Const (@{const_name prj}, udomT ->> T)
    9.11  fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT)
    9.12 @@ -68,7 +68,7 @@
    9.13  
    9.14  fun mk_cast (t, x) =
    9.15    capply_const (udomT, udomT)
    9.16 -  $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
    9.17 +  $ (capply_const (deflT, udomT ->> udomT) $ @{term "cast :: udom defl -> udom -> udom"} $ t)
    9.18    $ x
    9.19  
    9.20  (* manipulating theorems *)
    9.21 @@ -98,7 +98,7 @@
    9.22      val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl
    9.23  
    9.24      val deflT = Term.fastype_of defl
    9.25 -    val _ = if deflT = @{typ "defl"} then ()
    9.26 +    val _ = if deflT = @{typ "udom defl"} then ()
    9.27              else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT))
    9.28  
    9.29      (*lhs*)
    9.30 @@ -112,7 +112,7 @@
    9.31        |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
    9.32  
    9.33      (*set*)
    9.34 -    val set = @{const defl_set} $ defl
    9.35 +    val set = @{term "defl_set :: udom defl => udom => bool"} $ defl
    9.36  
    9.37      (*pcpodef*)
    9.38      val tac1 = rtac @{thm defl_set_bottom} 1
    10.1 --- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 05:15:31 2010 -0800
    10.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:34:41 2010 -0800
    10.3 @@ -477,7 +477,7 @@
    10.4  using upper_map_ID finite_deflation_upper_map
    10.5  unfolding upper_approx_def by (rule approx_chain_lemma1)
    10.6  
    10.7 -definition upper_defl :: "defl \<rightarrow> defl"
    10.8 +definition upper_defl :: "udom defl \<rightarrow> udom defl"
    10.9  where "upper_defl = defl_fun1 upper_approx upper_map"
   10.10  
   10.11  lemma cast_upper_defl:
    11.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 05:15:31 2010 -0800
    11.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 06:34:41 2010 -0800
    11.3 @@ -30,7 +30,7 @@
    11.4  
    11.5  definition
    11.6    foo_bar_baz_deflF ::
    11.7 -    "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
    11.8 +    "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
    11.9  where
   11.10    "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
   11.11      ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
   11.12 @@ -47,13 +47,13 @@
   11.13  
   11.14  text {* Individual type combinators are projected from the fixed point. *}
   11.15  
   11.16 -definition foo_defl :: "defl \<rightarrow> defl"
   11.17 +definition foo_defl :: "udom defl \<rightarrow> udom defl"
   11.18  where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
   11.19  
   11.20 -definition bar_defl :: "defl \<rightarrow> defl"
   11.21 +definition bar_defl :: "udom defl \<rightarrow> udom defl"
   11.22  where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
   11.23  
   11.24 -definition baz_defl :: "defl \<rightarrow> defl"
   11.25 +definition baz_defl :: "udom defl \<rightarrow> udom defl"
   11.26  where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
   11.27  
   11.28  lemma defl_apply_thms:
   11.29 @@ -103,7 +103,7 @@
   11.30  definition prj_foo :: "udom \<rightarrow> 'a foo"
   11.31  where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
   11.32  
   11.33 -definition defl_foo :: "'a foo itself \<Rightarrow> defl"
   11.34 +definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
   11.35  where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
   11.36  
   11.37  definition
   11.38 @@ -138,7 +138,7 @@
   11.39  definition prj_bar :: "udom \<rightarrow> 'a bar"
   11.40  where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
   11.41  
   11.42 -definition defl_bar :: "'a bar itself \<Rightarrow> defl"
   11.43 +definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
   11.44  where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
   11.45  
   11.46  definition
   11.47 @@ -173,7 +173,7 @@
   11.48  definition prj_baz :: "udom \<rightarrow> 'a baz"
   11.49  where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
   11.50  
   11.51 -definition defl_baz :: "'a baz itself \<Rightarrow> defl"
   11.52 +definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
   11.53  where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
   11.54  
   11.55  definition