# HG changeset patch
# User huffman
# Date 1289418155 28800
# Node ID d2e876d6da8c6d9288ec66edc40eabbc86e0e20e
# Parent  71283f31a27ff2378c80a637f8862a4b4d5c379d
rename class 'bifinite' to 'domain'

diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/Bifinite.thy
--- 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 *}
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/CompactBasis.thy
--- 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 *}
 
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/ConvexPD.thy
--- 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
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/HOLCF.thy
--- 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" *}
 
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/Library/Strict_Fun.thy
--- 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]:
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/LowerPD.thy
--- 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
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/Representable.thy
--- 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"}) ]
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/Tools/Domain/domain.ML
--- 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;
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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;
 
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/Tutorial/New_Domain.thy
--- 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.
 *}
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/UpperPD.thy
--- 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
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/ex/Domain_Proofs.thy
--- 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"
diff -r 71283f31a27f -r d2e876d6da8c src/HOLCF/ex/Powerdomain_ex.thy
--- 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