reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)

--- a/NEWS	Sun Dec 19 04:06:02 2010 -0800
+++ b/NEWS	Sun Dec 19 05:15:31 2010 -0800
@@ -487,8 +487,8 @@
 Accordingly, users of the definitional package must remove any
 'default_sort rep' declarations. INCOMPATIBILITY.
 
-* The old type classes 'profinite' and 'bifinite', along with the
-overloaded constant 'approx' have been removed. INCOMPATIBILITY.
+* 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

--- a/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -97,9 +97,10 @@
   "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
 
 lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
-proof
-  have *: "\<And>d. finite (approx_chain.place udom_approx `
-               Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
+proof -
+  obtain f :: "udom 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)
     apply (rule finite_vimageI)
     apply (rule Rep_fin_defl.finite_fixes)
@@ -107,11 +108,11 @@
     done
   have range_eq: "range Rep_compact_basis = {x. compact x}"
     using type_definition_compact_basis by (rule type_definition.Rep_range)
-  show "inj (\<lambda>d. set_encode
-    (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
+  have "inj (\<lambda>d. set_encode
+    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
     apply (rule inj_onI)
     apply (simp only: set_encode_eq *)
-    apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
+    apply (simp only: inj_image_eq_iff inj_f)
     apply (drule_tac f="image Rep_compact_basis" in arg_cong)
     apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
     apply (rule Rep_fin_defl_inject [THEN iffD1])
@@ -121,6 +122,7 @@
     apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
     apply (drule_tac x=z in spec, simp)
     done
+  thus ?thesis by - (rule exI)
 qed
 
 interpretation defl: ideal_completion below defl_principal Rep_defl

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -0,0 +1,275 @@
+(*  Title:      HOLCF/Bifinite.thy
+    Author:     Brian Huffman
+*)
+
+header {* Profinite and bifinite cpos *}
+
+theory Bifinite
+imports Map_Functions Countable
+begin
+
+default_sort cpo
+
+subsection {* Chains of finite deflations *}
+
+locale approx_chain =
+  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
+  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
+  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
+  assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)"
+begin
+
+lemma deflation_approx: "deflation (approx i)"
+using finite_deflation_approx by (rule finite_deflation_imp_deflation)
+
+lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+using deflation_approx by (rule deflation.idem)
+
+lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
+using deflation_approx by (rule deflation.below)
+
+lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
+apply (rule finite_deflation.finite_range)
+apply (rule finite_deflation_approx)
+done
+
+lemma compact_approx: "compact (approx n\<cdot>x)"
+apply (rule finite_deflation.compact)
+apply (rule finite_deflation_approx)
+done
+
+lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
+by (rule admD2, simp_all)
+
+end
+
+subsection {* Omega-profinite and bifinite domains *}
+
+class bifinite = pcpo +
+  assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
+
+class profinite = cpo +
+  assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
+
+subsection {* Building approx chains *}
+
+lemma approx_chain_iso:
+  assumes a: "approx_chain a"
+  assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
+  assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"
+  shows "approx_chain (\<lambda>i. f oo a i oo g)"
+proof -
+  have 1: "f oo g = ID" by (simp add: cfun_eqI)
+  have 2: "ep_pair f g" by (simp add: ep_pair_def)
+  from 1 2 show ?thesis
+    using a unfolding approx_chain_def
+    by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
+qed
+
+lemma approx_chain_u_map:
+  assumes "approx_chain a"
+  shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP u_map_ID finite_deflation_u_map)
+
+lemma approx_chain_sfun_map:
+  assumes "approx_chain a" and "approx_chain b"
+  shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
+
+lemma approx_chain_sprod_map:
+  assumes "approx_chain a" and "approx_chain b"
+  shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
+
+lemma approx_chain_ssum_map:
+  assumes "approx_chain a" and "approx_chain b"
+  shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
+
+lemma approx_chain_cfun_map:
+  assumes "approx_chain a" and "approx_chain b"
+  shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
+
+lemma approx_chain_cprod_map:
+  assumes "approx_chain a" and "approx_chain b"
+  shows "approx_chain (\<lambda>i. cprod_map\<cdot>(a i)\<cdot>(b i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP cprod_map_ID finite_deflation_cprod_map)
+
+text {* Approx chains for countable discrete types. *}
+
+definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
+  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
+
+lemma chain_discr_approx [simp]: "chain discr_approx"
+unfolding discr_approx_def
+by (rule chainI, simp add: monofun_cfun monofun_LAM)
+
+lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
+apply (rule cfun_eqI)
+apply (simp add: contlub_cfun_fun)
+apply (simp add: discr_approx_def)
+apply (case_tac x, simp)
+apply (rule lub_eqI)
+apply (rule is_lubI)
+apply (rule ub_rangeI, simp)
+apply (drule ub_rangeD)
+apply (erule rev_below_trans)
+apply simp
+apply (rule lessI)
+done
+
+lemma inj_on_undiscr [simp]: "inj_on undiscr A"
+using Discr_undiscr by (rule inj_on_inverseI)
+
+lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
+proof
+  fix x :: "'a discr u"
+  show "discr_approx i\<cdot>x \<sqsubseteq> x"
+    unfolding discr_approx_def
+    by (cases x, simp, simp)
+  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
+    unfolding discr_approx_def
+    by (cases x, simp, simp)
+  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
+  proof (rule finite_subset)
+    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
+    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
+      unfolding discr_approx_def
+      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
+    show "finite ?S"
+      by (simp add: finite_vimageI)
+  qed
+qed
+
+lemma discr_approx: "approx_chain discr_approx"
+using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
+by (rule approx_chain.intro)
+
+subsection {* Class instance proofs *}
+
+instance bifinite \<subseteq> profinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
+    using bifinite [where 'a='a]
+    by (fast intro!: approx_chain_u_map)
+qed
+
+instance u :: (profinite) bifinite
+  by default (rule profinite)
+
+text {*
+  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
+*}
+
+definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
+
+definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
+
+lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
+unfolding encode_cfun_def decode_cfun_def
+by (simp add: eta_cfun)
+
+lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
+unfolding encode_cfun_def decode_cfun_def
+apply (simp add: sfun_eq_iff strictify_cancel)
+apply (rule cfun_eqI, case_tac x, simp_all)
+done
+
+instance cfun :: (profinite, bifinite) bifinite
+proof
+  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
+    using profinite ..
+  obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
+    using bifinite ..
+  have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
+    using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
+  thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
+    by - (rule exI)
+qed
+
+text {*
+  Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
+*}
+
+definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
+
+definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
+
+lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
+unfolding encode_prod_u_def decode_prod_u_def
+by (case_tac x, simp, rename_tac y, case_tac y, simp)
+
+lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
+unfolding encode_prod_u_def decode_prod_u_def
+apply (case_tac y, simp, rename_tac a b)
+apply (case_tac a, simp, case_tac b, simp, simp)
+done
+
+instance prod :: (profinite, profinite) profinite
+proof
+  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
+    using profinite ..
+  obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
+    using profinite ..
+  have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
+    using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
+  thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
+    by - (rule exI)
+qed
+
+instance prod :: (bifinite, bifinite) bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
+    using bifinite [where 'a='a] and bifinite [where 'a='b]
+    by (fast intro!: approx_chain_cprod_map)
+qed
+
+instance sfun :: (bifinite, bifinite) bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
+    using bifinite [where 'a='a] and bifinite [where 'a='b]
+    by (fast intro!: approx_chain_sfun_map)
+qed
+
+instance sprod :: (bifinite, bifinite) bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
+    using bifinite [where 'a='a] and bifinite [where 'a='b]
+    by (fast intro!: approx_chain_sprod_map)
+qed
+
+instance ssum :: (bifinite, bifinite) bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
+    using bifinite [where 'a='a] and bifinite [where 'a='b]
+    by (fast intro!: approx_chain_ssum_map)
+qed
+
+lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
+by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
+
+instance unit :: bifinite
+  by default (fast intro!: approx_chain_unit)
+
+instance discr :: (countable) profinite
+  by default (fast intro!: discr_approx)
+
+instance lift :: (countable) bifinite
+proof
+  note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
+  obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
+    using profinite ..
+  hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
+    by (rule approx_chain_iso) simp_all
+  thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
+    by - (rule exI)
+qed
+
+end

--- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -468,6 +468,19 @@
 
 subsection {* Convex powerdomain is a domain *}
 
+lemma approx_chain_convex_map:
+  assumes "approx_chain a"
+  shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP convex_map_ID finite_deflation_convex_map)
+
+instance convex_pd :: ("domain") bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
+    using bifinite [where 'a='a]
+    by (fast intro!: approx_chain_convex_map)
+qed
+
 definition
   convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
 where

--- a/src/HOL/HOLCF/IsaMakefile	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/IsaMakefile	Sun Dec 19 05:15:31 2010 -0800
@@ -37,6 +37,7 @@
   ROOT.ML \
   Adm.thy \
   Algebraic.thy \
+  Bifinite.thy \
   Cfun.thy \
   Compact_Basis.thy \
   Completion.thy \

--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -609,6 +609,9 @@
 
 subsection {* Algebraic deflations are a bifinite domain *}
 
+instance defl :: bifinite
+  by default (fast intro!: defl_approx)
+
 instantiation defl :: liftdomain
 begin
 

--- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -460,6 +460,19 @@
 
 subsection {* Lower powerdomain is a domain *}
 
+lemma approx_chain_lower_map:
+  assumes "approx_chain a"
+  shows "approx_chain (\<lambda>i. lower_map\<cdot>(a i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP lower_map_ID finite_deflation_lower_map)
+
+instance lower_pd :: ("domain") bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a"
+    using bifinite [where 'a='a]
+    by (fast intro!: approx_chain_lower_map)
+qed
+
 definition
   lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
 where

--- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -48,41 +48,44 @@
 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 domain class.
-*}
+subsection {* Domains are bifinite *}
 
-interpretation compact_basis:
-  ideal_completion below Rep_compact_basis "approximants::'a::domain \<Rightarrow> _"
+lemma approx_chain_ep_cast:
+  assumes ep: "ep_pair (e::'a \<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"
 proof -
+  interpret ep_pair e p by fact
   obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
-  and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
+  and t: "t = (\<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"
-  interpret defl_approx: approx_chain approx
+  def approx \<equiv> "\<lambda>i. (p oo cast\<cdot>(defl_principal (Y i)) oo e) :: 'a \<rightarrow> 'a"
+  have "approx_chain approx"
   proof (rule approx_chain.intro)
     show "chain (\<lambda>i. approx i)"
       unfolding approx_def by (simp add: Y)
     show "(\<Squnion>i. approx i) = ID"
       unfolding approx_def
-      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
+      by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)
     show "\<And>i. finite_deflation (approx i)"
       unfolding approx_def
-      apply (rule domain.finite_deflation_p_d_e)
+      apply (rule 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)
+      apply (simp add: lub_distribs Y t [symmetric] cast_t)
       done
   qed
-  (* FIXME: why does show ?thesis fail here? *)
-  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
+  thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI)
 qed
 
+instance "domain" \<subseteq> bifinite
+by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
+
+instance predomain \<subseteq> profinite
+by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
+
 subsection {* Chains of approx functions *}
 
 definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
@@ -137,6 +140,8 @@
 
 subsection {* Type combinators *}
 
+default_sort bifinite
+
 definition
   defl_fun1 ::
     "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
@@ -166,7 +171,7 @@
   have 1: "\<And>a. finite_deflation
         (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
     apply (rule ep_pair.finite_deflation_e_d_p)
-    apply (rule approx_chain.ep_pair_udom [OF approx])
+    apply (rule ep_pair_udom [OF approx])
     apply (rule f, rule finite_deflation_Rep_fin_defl)
     done
   show ?thesis
@@ -279,6 +284,8 @@
   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
 *}
 
+default_sort pcpo
+
 lemma liftdomain_class_intro:
   assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
   assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
@@ -436,26 +443,6 @@
 
 subsubsection {* Continuous function space *}
 
-text {*
-  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
-*}
-
-definition
-  "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
-
-definition
-  "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
-
-lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
-unfolding encode_cfun_def decode_cfun_def
-by (simp add: eta_cfun)
-
-lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
-unfolding encode_cfun_def decode_cfun_def
-apply (simp add: sfun_eq_iff strictify_cancel)
-apply (rule cfun_eqI, case_tac x, simp_all)
-done
-
 instantiation cfun :: (predomain, "domain") liftdomain
 begin
 
@@ -540,26 +527,6 @@
 
 subsubsection {* Cartesian product *}
 
-text {*
-  Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
-*}
-
-definition
-  "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
-
-definition
-  "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
-
-lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
-unfolding encode_prod_u_def decode_prod_u_def
-by (case_tac x, simp, rename_tac y, case_tac y, simp)
-
-lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
-unfolding encode_prod_u_def decode_prod_u_def
-apply (case_tac y, simp, rename_tac a b)
-apply (case_tac a, simp, case_tac b, simp, simp)
-done
-
 instantiation prod :: (predomain, predomain) predomain
 begin
 
@@ -656,66 +623,18 @@
 
 subsubsection {* Discrete cpo *}
 
-definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
-  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
-
-lemma chain_discr_approx [simp]: "chain discr_approx"
-unfolding discr_approx_def
-by (rule chainI, simp add: monofun_cfun monofun_LAM)
-
-lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
-apply (rule cfun_eqI)
-apply (simp add: contlub_cfun_fun)
-apply (simp add: discr_approx_def)
-apply (case_tac x, simp)
-apply (rule lub_eqI)
-apply (rule is_lubI)
-apply (rule ub_rangeI, simp)
-apply (drule ub_rangeD)
-apply (erule rev_below_trans)
-apply simp
-apply (rule lessI)
-done
-
-lemma inj_on_undiscr [simp]: "inj_on undiscr A"
-using Discr_undiscr by (rule inj_on_inverseI)
-
-lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
-proof
-  fix x :: "'a discr u"
-  show "discr_approx i\<cdot>x \<sqsubseteq> x"
-    unfolding discr_approx_def
-    by (cases x, simp, simp)
-  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
-    unfolding discr_approx_def
-    by (cases x, simp, simp)
-  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
-  proof (rule finite_subset)
-    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
-    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
-      unfolding discr_approx_def
-      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
-    show "finite ?S"
-      by (simp add: finite_vimageI)
-  qed
-qed
-
-lemma discr_approx: "approx_chain discr_approx"
-using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
-by (rule approx_chain.intro)
-
 instantiation discr :: (countable) predomain
 begin
 
 definition
-  "liftemb = udom_emb discr_approx"
+  "(liftemb :: 'a discr u \<rightarrow> udom) = udom_emb discr_approx"
 
 definition
-  "liftprj = udom_prj discr_approx"
+  "(liftprj :: udom \<rightarrow> 'a discr u) = udom_prj discr_approx"
 
 definition
   "liftdefl (t::'a discr itself) =
-    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo liftprj)))"
+    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom \<rightarrow> 'a discr u))))"
 
 instance proof
   show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a discr u)"

--- a/src/HOL/HOLCF/Universal.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -5,7 +5,7 @@
 header {* A universal bifinite domain *}
 
 theory Universal
-imports Completion Deflation Nat_Bijection
+imports Bifinite Completion Nat_Bijection
 begin
 
 subsection {* Basis for universal domain *}
@@ -287,11 +287,8 @@
 text {* We use a locale to parameterize the construction over a chain
 of approx functions on the type to be embedded. *}
 
-locale approx_chain =
-  fixes approx :: "nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a"
-  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
-  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
-  assumes finite_deflation_approx: "\<And>i. finite_deflation (approx i)"
+locale bifinite_approx_chain = approx_chain +
+  constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
 begin
 
 subsubsection {* Choosing a maximal element from a finite set *}
@@ -408,30 +405,6 @@
  apply (simp add: choose_pos.simps)
 done
 
-subsubsection {* Properties of approx function *}
-
-lemma deflation_approx: "deflation (approx i)"
-using finite_deflation_approx by (rule finite_deflation_imp_deflation)
-
-lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
-using deflation_approx by (rule deflation.idem)
-
-lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
-using deflation_approx by (rule deflation.below)
-
-lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
-apply (rule finite_deflation.finite_range)
-apply (rule finite_deflation_approx)
-done
-
-lemma compact_approx: "compact (approx n\<cdot>x)"
-apply (rule finite_deflation.compact)
-apply (rule finite_deflation_approx)
-done
-
-lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
-by (rule admD2, simp_all)
-
 subsubsection {* Compact basis take function *}
 
 primrec
@@ -804,11 +777,8 @@
  apply (rule ubasis_until_less)
 done
 
-end
-
-sublocale approx_chain \<subseteq> compact_basis!:
-  ideal_completion below Rep_compact_basis
-    "approximants :: 'a \<Rightarrow> 'a compact_basis set"
+lemma ideal_completion:
+  "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)"
 proof
   fix w :: "'a"
   show "below.ideal (approximants w)"
@@ -873,9 +843,23 @@
     by (rule exI, rule inj_place)
 qed
 
+end
+
+interpretation compact_basis!:
+  ideal_completion below Rep_compact_basis
+    "approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set"
+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 "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)"
+    by (rule bifinite_approx_chain.ideal_completion)
+qed
+
 subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
 
-context approx_chain begin
+context bifinite_approx_chain begin
 
 definition
   udom_emb :: "'a \<rightarrow> udom"
@@ -915,10 +899,11 @@
 
 end
 
-abbreviation "udom_emb \<equiv> approx_chain.udom_emb"
-abbreviation "udom_prj \<equiv> approx_chain.udom_prj"
+abbreviation "udom_emb \<equiv> bifinite_approx_chain.udom_emb"
+abbreviation "udom_prj \<equiv> bifinite_approx_chain.udom_prj"
 
-lemmas ep_pair_udom = approx_chain.ep_pair_udom
+lemmas ep_pair_udom =
+  bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def]
 
 subsection {* Chain of approx functions for type \emph{udom} *}
 
@@ -1001,7 +986,7 @@
 apply (simp add: ubasis_until_same ubasis_le_refl)
 done
  
-lemma udom_approx: "approx_chain udom_approx"
+lemma udom_approx [simp]: "approx_chain udom_approx"
 proof
   show "chain (\<lambda>i. udom_approx i)"
     by (rule chain_udom_approx)
@@ -1009,6 +994,9 @@
     by (rule lub_udom_approx)
 qed
 
+instance udom :: bifinite
+  by default (fast intro: udom_approx)
+
 hide_const (open) node
 
 end

--- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 05:15:31 2010 -0800
@@ -455,6 +455,19 @@
 
 subsection {* Upper powerdomain is a domain *}
 
+lemma approx_chain_upper_map:
+  assumes "approx_chain a"
+  shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))"
+  using assms unfolding approx_chain_def
+  by (simp add: lub_APP upper_map_ID finite_deflation_upper_map)
+
+instance upper_pd :: ("domain") bifinite
+proof
+  show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a"
+    using bifinite [where 'a='a]
+    by (fast intro!: approx_chain_upper_map)
+qed
+
 definition
   upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
 where

--- a/src/HOL/IsaMakefile	Sun Dec 19 04:06:02 2010 -0800
+++ b/src/HOL/IsaMakefile	Sun Dec 19 05:15:31 2010 -0800
@@ -1404,6 +1404,7 @@
   HOLCF/ROOT.ML \
   HOLCF/Adm.thy \
   HOLCF/Algebraic.thy \
+  HOLCF/Bifinite.thy \
   HOLCF/Cfun.thy \
   HOLCF/Compact_Basis.thy \
   HOLCF/Completion.thy \