type 'defl' takes a type parameter again (cf. b525988432e9)
--- 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)'.
--- 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"
--- 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:
--- 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"
--- 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)
--- 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:
--- 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"}) ]
*}
--- 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
--- 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
--- 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:
--- 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