src/HOLCF/Bifinite.thy

 begin
 
 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.
-
-  A predomain is a cpo that, when lifted, becomes bifinite.
+  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 a domain.
 *}
 
 class predomain = cpo +
   fixes liftdefl :: "('a::cpo) itself \<Rightarrow> defl"
   fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom"

   assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a::cpo)) = liftemb oo liftprj"
 
 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"
   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'(_')))")
 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
-
-subsection {* Bifinite domains have a countable compact basis *}
+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 {* 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))"
     by (rule defl.obtain_principal_chain)
   def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"

     show "(\<Squnion>i. approx i) = ID"
       unfolding approx_def
       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])
       apply (rule is_ub_thelub, simp add: Y)
       apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL)

   "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
     udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
 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)"
 
 text {* Temporarily relax type constraints. *}

 
 text {* Restore original type constraints. *}
 
 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
 
 definition [simp]:

     done
 qed
 
 end
 
-subsection {* Lifted predomains are bifinite *}
+subsection {* Lifted predomains are domains *}
 
 instantiation u :: (predomain) liftdomain
 begin
 
 definition

 end
 
 lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
 by (rule defl_u_def)
 
-subsection {* Continuous function space is a bifinite domain *}
-
-instantiation cfun :: (bifinite, bifinite) liftdomain
+subsection {* Continuous function space is a domain *}
+
+text {* TODO: Allow argument type to be a predomain. *}
+
+instantiation cfun :: ("domain", "domain") liftdomain
 begin
 
 definition
   "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
 

 qed
 
 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.
 *}
 

     by (simp add: cast_sprod_defl cast_DEFL cfcomp1 sprod_map_map)
 qed
 
 end
 
-instantiation prod :: (bifinite, bifinite) bifinite
+instantiation prod :: ("domain", "domain") "domain"
 begin
 
 definition
   "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
 

 qed
 
 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 *}
-
-instantiation sprod :: (bifinite, bifinite) liftdomain
+subsection {* Strict product is a domain *}
+
+instantiation sprod :: ("domain", "domain") liftdomain
 begin
 
 definition
   "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
 

 qed
 
 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 *}
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"

     done
 qed
 
 end
 
-subsection {* Strict sum is a bifinite domain *}
-
-instantiation ssum :: (bifinite, bifinite) liftdomain
+subsection {* Strict sum is a domain *}
+
+instantiation ssum :: ("domain", "domain") liftdomain
 begin
 
 definition
   "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
 

 qed
 
 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 *}
 
 instantiation lift :: (countable) liftdomain