--- a/src/HOLCF/Bifinite.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Bifinite.thy Wed Nov 10 11:42:35 2010 -0800
@@ -11,10 +11,11 @@
subsection {* Class of bifinite domains *}
text {*
- We define a bifinite domain as a pcpo that is isomorphic to some
- algebraic deflation over the universal domain.
+ We define a ``domain'' as a pcpo that is isomorphic to some
+ algebraic deflation over the universal domain; this is equivalent
+ to being omega-bifinite.
- A predomain is a cpo that, when lifted, becomes bifinite.
+ A predomain is a cpo that, when lifted, becomes a domain.
*}
class predomain = cpo +
@@ -27,7 +28,7 @@
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
-class bifinite = predomain + pcpo +
+class "domain" = predomain + pcpo +
fixes emb :: "'a::cpo \<rightarrow> udom"
fixes prj :: "udom \<rightarrow> 'a::cpo"
fixes defl :: "'a itself \<Rightarrow> defl"
@@ -37,25 +38,25 @@
syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))")
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
-interpretation bifinite: pcpo_ep_pair emb prj
+interpretation "domain": pcpo_ep_pair emb prj
unfolding pcpo_ep_pair_def
by (rule ep_pair_emb_prj)
-lemmas emb_inverse = bifinite.e_inverse
-lemmas emb_prj_below = bifinite.e_p_below
-lemmas emb_eq_iff = bifinite.e_eq_iff
-lemmas emb_strict = bifinite.e_strict
-lemmas prj_strict = bifinite.p_strict
+lemmas emb_inverse = domain.e_inverse
+lemmas emb_prj_below = domain.e_p_below
+lemmas emb_eq_iff = domain.e_eq_iff
+lemmas emb_strict = domain.e_strict
+lemmas prj_strict = domain.p_strict
-subsection {* Bifinite domains have a countable compact basis *}
+subsection {* Domains have a countable compact basis *}
text {*
Eventually it should be possible to generalize this to an unpointed
- variant of the bifinite class.
+ variant of the domain class.
*}
interpretation compact_basis:
- ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
+ ideal_completion below Rep_compact_basis "approximants::'a::domain \<Rightarrow> _"
proof -
obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
@@ -70,7 +71,7 @@
by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
show "\<And>i. finite_deflation (approx i)"
unfolding approx_def
- apply (rule bifinite.finite_deflation_p_d_e)
+ apply (rule domain.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (rule defl.compact_principal)
apply (rule below_trans [OF monofun_cfun_fun])
@@ -254,14 +255,14 @@
using ssum_approx finite_deflation_ssum_map
unfolding ssum_defl_def by (rule cast_defl_fun2)
-subsection {* Lemma for proving bifinite instances *}
+subsection {* Lemma for proving domain instances *}
text {*
- A class of bifinite domains where @{const liftemb}, @{const liftprj},
+ A class of domains where @{const liftemb}, @{const liftprj},
and @{const liftdefl} are all defined in the standard way.
*}
-class liftdomain = bifinite +
+class liftdomain = "domain" +
assumes liftemb_eq: "liftemb = udom_emb u_approx oo u_map\<cdot>emb"
assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo udom_prj u_approx"
assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\<cdot>DEFL('a)"
@@ -299,15 +300,15 @@
setup {*
fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"})
- , (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"})
+ [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> 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 liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
*}
-subsection {* The universal domain is bifinite *}
+subsection {* The universal domain is a domain *}
instantiation udom :: liftdomain
begin
@@ -351,7 +352,7 @@
end
-subsection {* Lifted predomains are bifinite *}
+subsection {* Lifted predomains are domains *}
instantiation u :: (predomain) liftdomain
begin
@@ -390,9 +391,11 @@
lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
by (rule defl_u_def)
-subsection {* Continuous function space is a bifinite domain *}
+subsection {* Continuous function space is a domain *}
-instantiation cfun :: (bifinite, bifinite) liftdomain
+text {* TODO: Allow argument type to be a predomain. *}
+
+instantiation cfun :: ("domain", "domain") liftdomain
begin
definition
@@ -428,10 +431,10 @@
end
lemma DEFL_cfun:
- "DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<rightarrow> 'b::domain) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_cfun_def)
-subsection {* Cartesian product is a bifinite domain *}
+subsection {* Cartesian product is a domain *}
text {*
Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
@@ -484,7 +487,7 @@
end
-instantiation prod :: (bifinite, bifinite) bifinite
+instantiation prod :: ("domain", "domain") "domain"
begin
definition
@@ -510,16 +513,16 @@
end
lemma DEFL_prod:
- "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_prod_def)
lemma LIFTDEFL_prod:
"LIFTDEFL('a::predomain \<times> 'b::predomain) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
by (rule liftdefl_prod_def)
-subsection {* Strict product is a bifinite domain *}
+subsection {* Strict product is a domain *}
-instantiation sprod :: (bifinite, bifinite) liftdomain
+instantiation sprod :: ("domain", "domain") liftdomain
begin
definition
@@ -556,7 +559,7 @@
end
lemma DEFL_sprod:
- "DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sprod_def)
subsection {* Countable discrete cpos are predomains *}
@@ -648,9 +651,9 @@
end
-subsection {* Strict sum is a bifinite domain *}
+subsection {* Strict sum is a domain *}
-instantiation ssum :: (bifinite, bifinite) liftdomain
+instantiation ssum :: ("domain", "domain") liftdomain
begin
definition
@@ -686,7 +689,7 @@
end
lemma DEFL_ssum:
- "DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_ssum_def)
subsection {* Lifted countable types are bifinite domains *}
--- a/src/HOLCF/CompactBasis.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/CompactBasis.thy Wed Nov 10 11:42:35 2010 -0800
@@ -8,7 +8,7 @@
imports Bifinite
begin
-default_sort bifinite
+default_sort "domain"
subsection {* A compact basis for powerdomains *}
--- a/src/HOLCF/ConvexPD.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/ConvexPD.thy Wed Nov 10 11:42:35 2010 -0800
@@ -123,7 +123,7 @@
"{S::'a pd_basis set. convex_le.ideal S}"
by (fast intro: convex_le.ideal_principal)
-instantiation convex_pd :: (bifinite) below
+instantiation convex_pd :: ("domain") below
begin
definition
@@ -132,11 +132,11 @@
instance ..
end
-instance convex_pd :: (bifinite) po
+instance convex_pd :: ("domain") po
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_po)
-instance convex_pd :: (bifinite) cpo
+instance convex_pd :: ("domain") cpo
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_cpo)
@@ -155,7 +155,7 @@
lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: convex_pd.principal_induct, simp, simp)
-instance convex_pd :: (bifinite) pcpo
+instance convex_pd :: ("domain") pcpo
by intro_classes (fast intro: convex_pd_minimal)
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
@@ -440,7 +440,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Convex powerdomain is a bifinite domain *}
+subsection {* Convex powerdomain is a domain *}
definition
convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
@@ -460,7 +460,7 @@
using convex_approx finite_deflation_convex_map
unfolding convex_defl_def by (rule cast_defl_fun1)
-instantiation convex_pd :: (bifinite) liftdomain
+instantiation convex_pd :: ("domain") liftdomain
begin
definition
--- a/src/HOLCF/HOLCF.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/HOLCF.thy Wed Nov 10 11:42:35 2010 -0800
@@ -11,7 +11,7 @@
Powerdomains
begin
-default_sort bifinite
+default_sort "domain"
ML {* path_add "~~/src/HOLCF/Library" *}
--- a/src/HOLCF/Library/Strict_Fun.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Library/Strict_Fun.thy Wed Nov 10 11:42:35 2010 -0800
@@ -173,7 +173,7 @@
apply (erule (1) finite_deflation_sfun_map)
done
-instantiation sfun :: (bifinite, bifinite) liftdomain
+instantiation sfun :: ("domain", "domain") liftdomain
begin
definition
@@ -210,7 +210,7 @@
end
lemma DEFL_sfun [domain_defl_simps]:
- "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+ "DEFL('a \<rightarrow>! 'b) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sfun_def)
lemma isodefl_sfun [domain_isodefl]:
--- a/src/HOLCF/LowerPD.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/LowerPD.thy Wed Nov 10 11:42:35 2010 -0800
@@ -78,7 +78,7 @@
"{S::'a pd_basis set. lower_le.ideal S}"
by (fast intro: lower_le.ideal_principal)
-instantiation lower_pd :: (bifinite) below
+instantiation lower_pd :: ("domain") below
begin
definition
@@ -87,11 +87,11 @@
instance ..
end
-instance lower_pd :: (bifinite) po
+instance lower_pd :: ("domain") po
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_po)
-instance lower_pd :: (bifinite) cpo
+instance lower_pd :: ("domain") cpo
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_cpo)
@@ -110,7 +110,7 @@
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)
-instance lower_pd :: (bifinite) pcpo
+instance lower_pd :: ("domain") pcpo
by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
@@ -433,7 +433,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Lower powerdomain is a bifinite domain *}
+subsection {* Lower powerdomain is a domain *}
definition
lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
@@ -453,7 +453,7 @@
using lower_approx finite_deflation_lower_map
unfolding lower_defl_def by (rule cast_defl_fun1)
-instantiation lower_pd :: (bifinite) liftdomain
+instantiation lower_pd :: ("domain") liftdomain
begin
definition
--- a/src/HOLCF/Representable.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Representable.thy Wed Nov 10 11:42:35 2010 -0800
@@ -11,7 +11,7 @@
("Tools/Domain/domain_isomorphism.ML")
begin
-default_sort bifinite
+default_sort "domain"
subsection {* Representations of types *}
@@ -146,9 +146,9 @@
setup {*
fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"})
- , (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"})
+ [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> 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 liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
--- a/src/HOLCF/Tools/Domain/domain.ML Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain.ML Wed Nov 10 11:42:35 2010 -0800
@@ -185,7 +185,7 @@
end;
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
-fun rep_arg lazy = @{sort bifinite};
+fun rep_arg lazy = @{sort "domain"};
fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
| read_sort thy NONE = Sign.defaultS thy;
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 10 11:42:35 2010 -0800
@@ -429,15 +429,15 @@
val tmp_thy =
let
fun arity (vs, tbind, mx, _, _) =
- (Sign.full_name thy tbind, map the_sort vs, @{sort bifinite});
+ (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"});
in
fold AxClass.axiomatize_arity (map arity doms) tmp_thy
end;
(* check bifiniteness of right-hand sides *)
fun check_rhs (vs, tbind, mx, rhs, morphs) =
- if Sign.of_sort tmp_thy (rhs, @{sort bifinite}) then ()
- else error ("Type not of sort bifinite: " ^
+ if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
+ else error ("Type not of sort domain: " ^
quote (Syntax.string_of_typ_global tmp_thy rhs));
val _ = map check_rhs doms;
--- a/src/HOLCF/Tutorial/New_Domain.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Tutorial/New_Domain.thy Wed Nov 10 11:42:35 2010 -0800
@@ -13,10 +13,8 @@
package. This file should be merged with @{text Domain_ex.thy}.
*}
-default_sort bifinite
-
text {*
- Provided that @{text bifinite} is the default sort, the @{text new_domain}
+ Provided that @{text domain} is the default sort, the @{text new_domain}
package should work with any type definition supported by the old
domain package.
*}
--- a/src/HOLCF/UpperPD.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/UpperPD.thy Wed Nov 10 11:42:35 2010 -0800
@@ -76,7 +76,7 @@
"{S::'a pd_basis set. upper_le.ideal S}"
by (fast intro: upper_le.ideal_principal)
-instantiation upper_pd :: (bifinite) below
+instantiation upper_pd :: ("domain") below
begin
definition
@@ -85,11 +85,11 @@
instance ..
end
-instance upper_pd :: (bifinite) po
+instance upper_pd :: ("domain") po
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_po)
-instance upper_pd :: (bifinite) cpo
+instance upper_pd :: ("domain") cpo
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_cpo)
@@ -108,7 +108,7 @@
lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: upper_pd.principal_induct, simp, simp)
-instance upper_pd :: (bifinite) pcpo
+instance upper_pd :: ("domain") pcpo
by intro_classes (fast intro: upper_pd_minimal)
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
@@ -428,7 +428,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Upper powerdomain is a bifinite domain *}
+subsection {* Upper powerdomain is a domain *}
definition
upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
@@ -448,7 +448,7 @@
using upper_approx finite_deflation_upper_map
unfolding upper_defl_def by (rule cast_defl_fun1)
-instantiation upper_pd :: (bifinite) liftdomain
+instantiation upper_pd :: ("domain") liftdomain
begin
definition
--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 10 11:42:35 2010 -0800
@@ -94,7 +94,7 @@
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: (bifinite) liftdomain
+instantiation foo :: ("domain") liftdomain
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
@@ -129,7 +129,7 @@
end
-instantiation bar :: (bifinite) liftdomain
+instantiation bar :: ("domain") liftdomain
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
@@ -164,7 +164,7 @@
end
-instantiation baz :: (bifinite) liftdomain
+instantiation baz :: ("domain") liftdomain
begin
definition emb_baz :: "'a baz \<rightarrow> udom"
--- a/src/HOLCF/ex/Powerdomain_ex.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/ex/Powerdomain_ex.thy Wed Nov 10 11:42:35 2010 -0800
@@ -8,8 +8,6 @@
imports HOLCF
begin
-default_sort bifinite
-
subsection {* Monadic sorting example *}
domain ordering = LT | EQ | GT