reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
authorhuffman
Sun Dec 19 05:15:31 2010 -0800 (2010-12-19)
changeset 412863d7685a4a5ff
parent 41285 efd23c1d9886
child 41287 029a6fc1bfb8
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
NEWS
src/HOL/HOLCF/Algebraic.thy
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/IsaMakefile
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/UpperPD.thy
src/HOL/IsaMakefile
     1.1 --- a/NEWS	Sun Dec 19 04:06:02 2010 -0800
     1.2 +++ b/NEWS	Sun Dec 19 05:15:31 2010 -0800
     1.3 @@ -487,8 +487,8 @@
     1.4  Accordingly, users of the definitional package must remove any
     1.5  'default_sort rep' declarations. INCOMPATIBILITY.
     1.6  
     1.7 -* The old type classes 'profinite' and 'bifinite', along with the
     1.8 -overloaded constant 'approx' have been removed. INCOMPATIBILITY.
     1.9 +* The 'bifinite' class no longer fixes a constant 'approx'; the class
    1.10 +now just asserts that such a function exists. INCOMPATIBILITY.
    1.11  
    1.12  * The type 'udom alg_defl' has been replaced by the non-parameterized
    1.13  type 'defl'. HOLCF no longer defines an embedding of type defl into
     2.1 --- a/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 04:06:02 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Sun Dec 19 05:15:31 2010 -0800
     2.3 @@ -97,9 +97,10 @@
     2.4    "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
     2.5  
     2.6  lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
     2.7 -proof
     2.8 -  have *: "\<And>d. finite (approx_chain.place udom_approx `
     2.9 -               Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
    2.10 +proof -
    2.11 +  obtain f :: "udom compact_basis \<Rightarrow> nat" where inj_f: "inj f"
    2.12 +    using compact_basis.countable ..
    2.13 +  have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
    2.14      apply (rule finite_imageI)
    2.15      apply (rule finite_vimageI)
    2.16      apply (rule Rep_fin_defl.finite_fixes)
    2.17 @@ -107,11 +108,11 @@
    2.18      done
    2.19    have range_eq: "range Rep_compact_basis = {x. compact x}"
    2.20      using type_definition_compact_basis by (rule type_definition.Rep_range)
    2.21 -  show "inj (\<lambda>d. set_encode
    2.22 -    (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
    2.23 +  have "inj (\<lambda>d. set_encode
    2.24 +    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
    2.25      apply (rule inj_onI)
    2.26      apply (simp only: set_encode_eq *)
    2.27 -    apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
    2.28 +    apply (simp only: inj_image_eq_iff inj_f)
    2.29      apply (drule_tac f="image Rep_compact_basis" in arg_cong)
    2.30      apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
    2.31      apply (rule Rep_fin_defl_inject [THEN iffD1])
    2.32 @@ -121,6 +122,7 @@
    2.33      apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
    2.34      apply (drule_tac x=z in spec, simp)
    2.35      done
    2.36 +  thus ?thesis by - (rule exI)
    2.37  qed
    2.38  
    2.39  interpretation defl: ideal_completion below defl_principal Rep_defl
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
     3.3 @@ -0,0 +1,275 @@
     3.4 +(*  Title:      HOLCF/Bifinite.thy
     3.5 +    Author:     Brian Huffman
     3.6 +*)
     3.7 +
     3.8 +header {* Profinite and bifinite cpos *}
     3.9 +
    3.10 +theory Bifinite
    3.11 +imports Map_Functions Countable
    3.12 +begin
    3.13 +
    3.14 +default_sort cpo
    3.15 +
    3.16 +subsection {* Chains of finite deflations *}
    3.17 +
    3.18 +locale approx_chain =
    3.19 +  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
    3.20 +  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
    3.21 +  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
    3.22 +  assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)"
    3.23 +begin
    3.24 +
    3.25 +lemma deflation_approx: "deflation (approx i)"
    3.26 +using finite_deflation_approx by (rule finite_deflation_imp_deflation)
    3.27 +
    3.28 +lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    3.29 +using deflation_approx by (rule deflation.idem)
    3.30 +
    3.31 +lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
    3.32 +using deflation_approx by (rule deflation.below)
    3.33 +
    3.34 +lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
    3.35 +apply (rule finite_deflation.finite_range)
    3.36 +apply (rule finite_deflation_approx)
    3.37 +done
    3.38 +
    3.39 +lemma compact_approx: "compact (approx n\<cdot>x)"
    3.40 +apply (rule finite_deflation.compact)
    3.41 +apply (rule finite_deflation_approx)
    3.42 +done
    3.43 +
    3.44 +lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
    3.45 +by (rule admD2, simp_all)
    3.46 +
    3.47 +end
    3.48 +
    3.49 +subsection {* Omega-profinite and bifinite domains *}
    3.50 +
    3.51 +class bifinite = pcpo +
    3.52 +  assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
    3.53 +
    3.54 +class profinite = cpo +
    3.55 +  assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
    3.56 +
    3.57 +subsection {* Building approx chains *}
    3.58 +
    3.59 +lemma approx_chain_iso:
    3.60 +  assumes a: "approx_chain a"
    3.61 +  assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
    3.62 +  assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"
    3.63 +  shows "approx_chain (\<lambda>i. f oo a i oo g)"
    3.64 +proof -
    3.65 +  have 1: "f oo g = ID" by (simp add: cfun_eqI)
    3.66 +  have 2: "ep_pair f g" by (simp add: ep_pair_def)
    3.67 +  from 1 2 show ?thesis
    3.68 +    using a unfolding approx_chain_def
    3.69 +    by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
    3.70 +qed
    3.71 +
    3.72 +lemma approx_chain_u_map:
    3.73 +  assumes "approx_chain a"
    3.74 +  shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))"
    3.75 +  using assms unfolding approx_chain_def
    3.76 +  by (simp add: lub_APP u_map_ID finite_deflation_u_map)
    3.77 +
    3.78 +lemma approx_chain_sfun_map:
    3.79 +  assumes "approx_chain a" and "approx_chain b"
    3.80 +  shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))"
    3.81 +  using assms unfolding approx_chain_def
    3.82 +  by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
    3.83 +
    3.84 +lemma approx_chain_sprod_map:
    3.85 +  assumes "approx_chain a" and "approx_chain b"
    3.86 +  shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))"
    3.87 +  using assms unfolding approx_chain_def
    3.88 +  by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
    3.89 +
    3.90 +lemma approx_chain_ssum_map:
    3.91 +  assumes "approx_chain a" and "approx_chain b"
    3.92 +  shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))"
    3.93 +  using assms unfolding approx_chain_def
    3.94 +  by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
    3.95 +
    3.96 +lemma approx_chain_cfun_map:
    3.97 +  assumes "approx_chain a" and "approx_chain b"
    3.98 +  shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
    3.99 +  using assms unfolding approx_chain_def
   3.100 +  by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
   3.101 +
   3.102 +lemma approx_chain_cprod_map:
   3.103 +  assumes "approx_chain a" and "approx_chain b"
   3.104 +  shows "approx_chain (\<lambda>i. cprod_map\<cdot>(a i)\<cdot>(b i))"
   3.105 +  using assms unfolding approx_chain_def
   3.106 +  by (simp add: lub_APP cprod_map_ID finite_deflation_cprod_map)
   3.107 +
   3.108 +text {* Approx chains for countable discrete types. *}
   3.109 +
   3.110 +definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   3.111 +  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
   3.112 +
   3.113 +lemma chain_discr_approx [simp]: "chain discr_approx"
   3.114 +unfolding discr_approx_def
   3.115 +by (rule chainI, simp add: monofun_cfun monofun_LAM)
   3.116 +
   3.117 +lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
   3.118 +apply (rule cfun_eqI)
   3.119 +apply (simp add: contlub_cfun_fun)
   3.120 +apply (simp add: discr_approx_def)
   3.121 +apply (case_tac x, simp)
   3.122 +apply (rule lub_eqI)
   3.123 +apply (rule is_lubI)
   3.124 +apply (rule ub_rangeI, simp)
   3.125 +apply (drule ub_rangeD)
   3.126 +apply (erule rev_below_trans)
   3.127 +apply simp
   3.128 +apply (rule lessI)
   3.129 +done
   3.130 +
   3.131 +lemma inj_on_undiscr [simp]: "inj_on undiscr A"
   3.132 +using Discr_undiscr by (rule inj_on_inverseI)
   3.133 +
   3.134 +lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
   3.135 +proof
   3.136 +  fix x :: "'a discr u"
   3.137 +  show "discr_approx i\<cdot>x \<sqsubseteq> x"
   3.138 +    unfolding discr_approx_def
   3.139 +    by (cases x, simp, simp)
   3.140 +  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
   3.141 +    unfolding discr_approx_def
   3.142 +    by (cases x, simp, simp)
   3.143 +  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
   3.144 +  proof (rule finite_subset)
   3.145 +    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
   3.146 +    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
   3.147 +      unfolding discr_approx_def
   3.148 +      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
   3.149 +    show "finite ?S"
   3.150 +      by (simp add: finite_vimageI)
   3.151 +  qed
   3.152 +qed
   3.153 +
   3.154 +lemma discr_approx: "approx_chain discr_approx"
   3.155 +using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
   3.156 +by (rule approx_chain.intro)
   3.157 +
   3.158 +subsection {* Class instance proofs *}
   3.159 +
   3.160 +instance bifinite \<subseteq> profinite
   3.161 +proof
   3.162 +  show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
   3.163 +    using bifinite [where 'a='a]
   3.164 +    by (fast intro!: approx_chain_u_map)
   3.165 +qed
   3.166 +
   3.167 +instance u :: (profinite) bifinite
   3.168 +  by default (rule profinite)
   3.169 +
   3.170 +text {*
   3.171 +  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
   3.172 +*}
   3.173 +
   3.174 +definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
   3.175 +
   3.176 +definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
   3.177 +
   3.178 +lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
   3.179 +unfolding encode_cfun_def decode_cfun_def
   3.180 +by (simp add: eta_cfun)
   3.181 +
   3.182 +lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
   3.183 +unfolding encode_cfun_def decode_cfun_def
   3.184 +apply (simp add: sfun_eq_iff strictify_cancel)
   3.185 +apply (rule cfun_eqI, case_tac x, simp_all)
   3.186 +done
   3.187 +
   3.188 +instance cfun :: (profinite, bifinite) bifinite
   3.189 +proof
   3.190 +  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
   3.191 +    using profinite ..
   3.192 +  obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
   3.193 +    using bifinite ..
   3.194 +  have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
   3.195 +    using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
   3.196 +  thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
   3.197 +    by - (rule exI)
   3.198 +qed
   3.199 +
   3.200 +text {*
   3.201 +  Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
   3.202 +*}
   3.203 +
   3.204 +definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
   3.205 +
   3.206 +definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
   3.207 +
   3.208 +lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
   3.209 +unfolding encode_prod_u_def decode_prod_u_def
   3.210 +by (case_tac x, simp, rename_tac y, case_tac y, simp)
   3.211 +
   3.212 +lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
   3.213 +unfolding encode_prod_u_def decode_prod_u_def
   3.214 +apply (case_tac y, simp, rename_tac a b)
   3.215 +apply (case_tac a, simp, case_tac b, simp, simp)
   3.216 +done
   3.217 +
   3.218 +instance prod :: (profinite, profinite) profinite
   3.219 +proof
   3.220 +  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
   3.221 +    using profinite ..
   3.222 +  obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
   3.223 +    using profinite ..
   3.224 +  have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
   3.225 +    using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
   3.226 +  thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
   3.227 +    by - (rule exI)
   3.228 +qed
   3.229 +
   3.230 +instance prod :: (bifinite, bifinite) bifinite
   3.231 +proof
   3.232 +  show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
   3.233 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   3.234 +    by (fast intro!: approx_chain_cprod_map)
   3.235 +qed
   3.236 +
   3.237 +instance sfun :: (bifinite, bifinite) bifinite
   3.238 +proof
   3.239 +  show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
   3.240 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   3.241 +    by (fast intro!: approx_chain_sfun_map)
   3.242 +qed
   3.243 +
   3.244 +instance sprod :: (bifinite, bifinite) bifinite
   3.245 +proof
   3.246 +  show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
   3.247 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   3.248 +    by (fast intro!: approx_chain_sprod_map)
   3.249 +qed
   3.250 +
   3.251 +instance ssum :: (bifinite, bifinite) bifinite
   3.252 +proof
   3.253 +  show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
   3.254 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   3.255 +    by (fast intro!: approx_chain_ssum_map)
   3.256 +qed
   3.257 +
   3.258 +lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
   3.259 +by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
   3.260 +
   3.261 +instance unit :: bifinite
   3.262 +  by default (fast intro!: approx_chain_unit)
   3.263 +
   3.264 +instance discr :: (countable) profinite
   3.265 +  by default (fast intro!: discr_approx)
   3.266 +
   3.267 +instance lift :: (countable) bifinite
   3.268 +proof
   3.269 +  note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
   3.270 +  obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
   3.271 +    using profinite ..
   3.272 +  hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
   3.273 +    by (rule approx_chain_iso) simp_all
   3.274 +  thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
   3.275 +    by - (rule exI)
   3.276 +qed
   3.277 +
   3.278 +end
     4.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 04:06:02 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 05:15:31 2010 -0800
     4.3 @@ -468,6 +468,19 @@
     4.4  
     4.5  subsection {* Convex powerdomain is a domain *}
     4.6  
     4.7 +lemma approx_chain_convex_map:
     4.8 +  assumes "approx_chain a"
     4.9 +  shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))"
    4.10 +  using assms unfolding approx_chain_def
    4.11 +  by (simp add: lub_APP convex_map_ID finite_deflation_convex_map)
    4.12 +
    4.13 +instance convex_pd :: ("domain") bifinite
    4.14 +proof
    4.15 +  show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
    4.16 +    using bifinite [where 'a='a]
    4.17 +    by (fast intro!: approx_chain_convex_map)
    4.18 +qed
    4.19 +
    4.20  definition
    4.21    convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
    4.22  where
     5.1 --- a/src/HOL/HOLCF/IsaMakefile	Sun Dec 19 04:06:02 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/IsaMakefile	Sun Dec 19 05:15:31 2010 -0800
     5.3 @@ -37,6 +37,7 @@
     5.4    ROOT.ML \
     5.5    Adm.thy \
     5.6    Algebraic.thy \
     5.7 +  Bifinite.thy \
     5.8    Cfun.thy \
     5.9    Compact_Basis.thy \
    5.10    Completion.thy \
     6.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 04:06:02 2010 -0800
     6.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
     6.3 @@ -609,6 +609,9 @@
     6.4  
     6.5  subsection {* Algebraic deflations are a bifinite domain *}
     6.6  
     6.7 +instance defl :: bifinite
     6.8 +  by default (fast intro!: defl_approx)
     6.9 +
    6.10  instantiation defl :: liftdomain
    6.11  begin
    6.12  
     7.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 04:06:02 2010 -0800
     7.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 05:15:31 2010 -0800
     7.3 @@ -460,6 +460,19 @@
     7.4  
     7.5  subsection {* Lower powerdomain is a domain *}
     7.6  
     7.7 +lemma approx_chain_lower_map:
     7.8 +  assumes "approx_chain a"
     7.9 +  shows "approx_chain (\<lambda>i. lower_map\<cdot>(a i))"
    7.10 +  using assms unfolding approx_chain_def
    7.11 +  by (simp add: lub_APP lower_map_ID finite_deflation_lower_map)
    7.12 +
    7.13 +instance lower_pd :: ("domain") bifinite
    7.14 +proof
    7.15 +  show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a"
    7.16 +    using bifinite [where 'a='a]
    7.17 +    by (fast intro!: approx_chain_lower_map)
    7.18 +qed
    7.19 +
    7.20  definition
    7.21    lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
    7.22  where
     8.1 --- a/src/HOL/HOLCF/Representable.thy	Sun Dec 19 04:06:02 2010 -0800
     8.2 +++ b/src/HOL/HOLCF/Representable.thy	Sun Dec 19 05:15:31 2010 -0800
     8.3 @@ -48,41 +48,44 @@
     8.4  lemmas emb_strict = domain.e_strict
     8.5  lemmas prj_strict = domain.p_strict
     8.6  
     8.7 -subsection {* Domains have a countable compact basis *}
     8.8 -
     8.9 -text {*
    8.10 -  Eventually it should be possible to generalize this to an unpointed
    8.11 -  variant of the domain class.
    8.12 -*}
    8.13 +subsection {* Domains are bifinite *}
    8.14  
    8.15 -interpretation compact_basis:
    8.16 -  ideal_completion below Rep_compact_basis "approximants::'a::domain \<Rightarrow> _"
    8.17 +lemma approx_chain_ep_cast:
    8.18 +  assumes ep: "ep_pair (e::'a \<rightarrow> udom) (p::udom \<rightarrow> 'a)"
    8.19 +  assumes cast_t: "cast\<cdot>t = e oo p"
    8.20 +  shows "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
    8.21  proof -
    8.22 +  interpret ep_pair e p by fact
    8.23    obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
    8.24 -  and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))"
    8.25 +  and t: "t = (\<Squnion>i. defl_principal (Y i))"
    8.26      by (rule defl.obtain_principal_chain)
    8.27 -  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
    8.28 -  interpret defl_approx: approx_chain approx
    8.29 +  def approx \<equiv> "\<lambda>i. (p oo cast\<cdot>(defl_principal (Y i)) oo e) :: 'a \<rightarrow> 'a"
    8.30 +  have "approx_chain approx"
    8.31    proof (rule approx_chain.intro)
    8.32      show "chain (\<lambda>i. approx i)"
    8.33        unfolding approx_def by (simp add: Y)
    8.34      show "(\<Squnion>i. approx i) = ID"
    8.35        unfolding approx_def
    8.36 -      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
    8.37 +      by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)
    8.38      show "\<And>i. finite_deflation (approx i)"
    8.39        unfolding approx_def
    8.40 -      apply (rule domain.finite_deflation_p_d_e)
    8.41 +      apply (rule finite_deflation_p_d_e)
    8.42        apply (rule finite_deflation_cast)
    8.43        apply (rule defl.compact_principal)
    8.44        apply (rule below_trans [OF monofun_cfun_fun])
    8.45        apply (rule is_ub_thelub, simp add: Y)
    8.46 -      apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL)
    8.47 +      apply (simp add: lub_distribs Y t [symmetric] cast_t)
    8.48        done
    8.49    qed
    8.50 -  (* FIXME: why does show ?thesis fail here? *)
    8.51 -  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
    8.52 +  thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI)
    8.53  qed
    8.54  
    8.55 +instance "domain" \<subseteq> bifinite
    8.56 +by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
    8.57 +
    8.58 +instance predomain \<subseteq> profinite
    8.59 +by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
    8.60 +
    8.61  subsection {* Chains of approx functions *}
    8.62  
    8.63  definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
    8.64 @@ -137,6 +140,8 @@
    8.65  
    8.66  subsection {* Type combinators *}
    8.67  
    8.68 +default_sort bifinite
    8.69 +
    8.70  definition
    8.71    defl_fun1 ::
    8.72      "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)"
    8.73 @@ -166,7 +171,7 @@
    8.74    have 1: "\<And>a. finite_deflation
    8.75          (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
    8.76      apply (rule ep_pair.finite_deflation_e_d_p)
    8.77 -    apply (rule approx_chain.ep_pair_udom [OF approx])
    8.78 +    apply (rule ep_pair_udom [OF approx])
    8.79      apply (rule f, rule finite_deflation_Rep_fin_defl)
    8.80      done
    8.81    show ?thesis
    8.82 @@ -279,6 +284,8 @@
    8.83    , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
    8.84  *}
    8.85  
    8.86 +default_sort pcpo
    8.87 +
    8.88  lemma liftdomain_class_intro:
    8.89    assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb"
    8.90    assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) = u_map\<cdot>prj oo udom_prj u_approx"
    8.91 @@ -436,26 +443,6 @@
    8.92  
    8.93  subsubsection {* Continuous function space *}
    8.94  
    8.95 -text {*
    8.96 -  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
    8.97 -*}
    8.98 -
    8.99 -definition
   8.100 -  "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
   8.101 -
   8.102 -definition
   8.103 -  "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
   8.104 -
   8.105 -lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
   8.106 -unfolding encode_cfun_def decode_cfun_def
   8.107 -by (simp add: eta_cfun)
   8.108 -
   8.109 -lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
   8.110 -unfolding encode_cfun_def decode_cfun_def
   8.111 -apply (simp add: sfun_eq_iff strictify_cancel)
   8.112 -apply (rule cfun_eqI, case_tac x, simp_all)
   8.113 -done
   8.114 -
   8.115  instantiation cfun :: (predomain, "domain") liftdomain
   8.116  begin
   8.117  
   8.118 @@ -540,26 +527,6 @@
   8.119  
   8.120  subsubsection {* Cartesian product *}
   8.121  
   8.122 -text {*
   8.123 -  Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
   8.124 -*}
   8.125 -
   8.126 -definition
   8.127 -  "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
   8.128 -
   8.129 -definition
   8.130 -  "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
   8.131 -
   8.132 -lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
   8.133 -unfolding encode_prod_u_def decode_prod_u_def
   8.134 -by (case_tac x, simp, rename_tac y, case_tac y, simp)
   8.135 -
   8.136 -lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
   8.137 -unfolding encode_prod_u_def decode_prod_u_def
   8.138 -apply (case_tac y, simp, rename_tac a b)
   8.139 -apply (case_tac a, simp, case_tac b, simp, simp)
   8.140 -done
   8.141 -
   8.142  instantiation prod :: (predomain, predomain) predomain
   8.143  begin
   8.144  
   8.145 @@ -656,66 +623,18 @@
   8.146  
   8.147  subsubsection {* Discrete cpo *}
   8.148  
   8.149 -definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   8.150 -  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
   8.151 -
   8.152 -lemma chain_discr_approx [simp]: "chain discr_approx"
   8.153 -unfolding discr_approx_def
   8.154 -by (rule chainI, simp add: monofun_cfun monofun_LAM)
   8.155 -
   8.156 -lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
   8.157 -apply (rule cfun_eqI)
   8.158 -apply (simp add: contlub_cfun_fun)
   8.159 -apply (simp add: discr_approx_def)
   8.160 -apply (case_tac x, simp)
   8.161 -apply (rule lub_eqI)
   8.162 -apply (rule is_lubI)
   8.163 -apply (rule ub_rangeI, simp)
   8.164 -apply (drule ub_rangeD)
   8.165 -apply (erule rev_below_trans)
   8.166 -apply simp
   8.167 -apply (rule lessI)
   8.168 -done
   8.169 -
   8.170 -lemma inj_on_undiscr [simp]: "inj_on undiscr A"
   8.171 -using Discr_undiscr by (rule inj_on_inverseI)
   8.172 -
   8.173 -lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
   8.174 -proof
   8.175 -  fix x :: "'a discr u"
   8.176 -  show "discr_approx i\<cdot>x \<sqsubseteq> x"
   8.177 -    unfolding discr_approx_def
   8.178 -    by (cases x, simp, simp)
   8.179 -  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
   8.180 -    unfolding discr_approx_def
   8.181 -    by (cases x, simp, simp)
   8.182 -  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
   8.183 -  proof (rule finite_subset)
   8.184 -    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
   8.185 -    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
   8.186 -      unfolding discr_approx_def
   8.187 -      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
   8.188 -    show "finite ?S"
   8.189 -      by (simp add: finite_vimageI)
   8.190 -  qed
   8.191 -qed
   8.192 -
   8.193 -lemma discr_approx: "approx_chain discr_approx"
   8.194 -using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
   8.195 -by (rule approx_chain.intro)
   8.196 -
   8.197  instantiation discr :: (countable) predomain
   8.198  begin
   8.199  
   8.200  definition
   8.201 -  "liftemb = udom_emb discr_approx"
   8.202 +  "(liftemb :: 'a discr u \<rightarrow> udom) = udom_emb discr_approx"
   8.203  
   8.204  definition
   8.205 -  "liftprj = udom_prj discr_approx"
   8.206 +  "(liftprj :: udom \<rightarrow> 'a discr u) = udom_prj discr_approx"
   8.207  
   8.208  definition
   8.209    "liftdefl (t::'a discr itself) =
   8.210 -    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo liftprj)))"
   8.211 +    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom \<rightarrow> 'a discr u))))"
   8.212  
   8.213  instance proof
   8.214    show "ep_pair liftemb (liftprj :: udom \<rightarrow> 'a discr u)"
     9.1 --- a/src/HOL/HOLCF/Universal.thy	Sun Dec 19 04:06:02 2010 -0800
     9.2 +++ b/src/HOL/HOLCF/Universal.thy	Sun Dec 19 05:15:31 2010 -0800
     9.3 @@ -5,7 +5,7 @@
     9.4  header {* A universal bifinite domain *}
     9.5  
     9.6  theory Universal
     9.7 -imports Completion Deflation Nat_Bijection
     9.8 +imports Bifinite Completion Nat_Bijection
     9.9  begin
    9.10  
    9.11  subsection {* Basis for universal domain *}
    9.12 @@ -287,11 +287,8 @@
    9.13  text {* We use a locale to parameterize the construction over a chain
    9.14  of approx functions on the type to be embedded. *}
    9.15  
    9.16 -locale approx_chain =
    9.17 -  fixes approx :: "nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a"
    9.18 -  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
    9.19 -  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
    9.20 -  assumes finite_deflation_approx: "\<And>i. finite_deflation (approx i)"
    9.21 +locale bifinite_approx_chain = approx_chain +
    9.22 +  constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
    9.23  begin
    9.24  
    9.25  subsubsection {* Choosing a maximal element from a finite set *}
    9.26 @@ -408,30 +405,6 @@
    9.27   apply (simp add: choose_pos.simps)
    9.28  done
    9.29  
    9.30 -subsubsection {* Properties of approx function *}
    9.31 -
    9.32 -lemma deflation_approx: "deflation (approx i)"
    9.33 -using finite_deflation_approx by (rule finite_deflation_imp_deflation)
    9.34 -
    9.35 -lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    9.36 -using deflation_approx by (rule deflation.idem)
    9.37 -
    9.38 -lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
    9.39 -using deflation_approx by (rule deflation.below)
    9.40 -
    9.41 -lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
    9.42 -apply (rule finite_deflation.finite_range)
    9.43 -apply (rule finite_deflation_approx)
    9.44 -done
    9.45 -
    9.46 -lemma compact_approx: "compact (approx n\<cdot>x)"
    9.47 -apply (rule finite_deflation.compact)
    9.48 -apply (rule finite_deflation_approx)
    9.49 -done
    9.50 -
    9.51 -lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
    9.52 -by (rule admD2, simp_all)
    9.53 -
    9.54  subsubsection {* Compact basis take function *}
    9.55  
    9.56  primrec
    9.57 @@ -804,11 +777,8 @@
    9.58   apply (rule ubasis_until_less)
    9.59  done
    9.60  
    9.61 -end
    9.62 -
    9.63 -sublocale approx_chain \<subseteq> compact_basis!:
    9.64 -  ideal_completion below Rep_compact_basis
    9.65 -    "approximants :: 'a \<Rightarrow> 'a compact_basis set"
    9.66 +lemma ideal_completion:
    9.67 +  "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)"
    9.68  proof
    9.69    fix w :: "'a"
    9.70    show "below.ideal (approximants w)"
    9.71 @@ -873,9 +843,23 @@
    9.72      by (rule exI, rule inj_place)
    9.73  qed
    9.74  
    9.75 +end
    9.76 +
    9.77 +interpretation compact_basis!:
    9.78 +  ideal_completion below Rep_compact_basis
    9.79 +    "approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set"
    9.80 +proof -
    9.81 +  obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a"
    9.82 +    using bifinite ..
    9.83 +  hence "bifinite_approx_chain a"
    9.84 +    unfolding bifinite_approx_chain_def .
    9.85 +  thus "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)"
    9.86 +    by (rule bifinite_approx_chain.ideal_completion)
    9.87 +qed
    9.88 +
    9.89  subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
    9.90  
    9.91 -context approx_chain begin
    9.92 +context bifinite_approx_chain begin
    9.93  
    9.94  definition
    9.95    udom_emb :: "'a \<rightarrow> udom"
    9.96 @@ -915,10 +899,11 @@
    9.97  
    9.98  end
    9.99  
   9.100 -abbreviation "udom_emb \<equiv> approx_chain.udom_emb"
   9.101 -abbreviation "udom_prj \<equiv> approx_chain.udom_prj"
   9.102 +abbreviation "udom_emb \<equiv> bifinite_approx_chain.udom_emb"
   9.103 +abbreviation "udom_prj \<equiv> bifinite_approx_chain.udom_prj"
   9.104  
   9.105 -lemmas ep_pair_udom = approx_chain.ep_pair_udom
   9.106 +lemmas ep_pair_udom =
   9.107 +  bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def]
   9.108  
   9.109  subsection {* Chain of approx functions for type \emph{udom} *}
   9.110  
   9.111 @@ -1001,7 +986,7 @@
   9.112  apply (simp add: ubasis_until_same ubasis_le_refl)
   9.113  done
   9.114   
   9.115 -lemma udom_approx: "approx_chain udom_approx"
   9.116 +lemma udom_approx [simp]: "approx_chain udom_approx"
   9.117  proof
   9.118    show "chain (\<lambda>i. udom_approx i)"
   9.119      by (rule chain_udom_approx)
   9.120 @@ -1009,6 +994,9 @@
   9.121      by (rule lub_udom_approx)
   9.122  qed
   9.123  
   9.124 +instance udom :: bifinite
   9.125 +  by default (fast intro: udom_approx)
   9.126 +
   9.127  hide_const (open) node
   9.128  
   9.129  end
    10.1 --- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 04:06:02 2010 -0800
    10.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 05:15:31 2010 -0800
    10.3 @@ -455,6 +455,19 @@
    10.4  
    10.5  subsection {* Upper powerdomain is a domain *}
    10.6  
    10.7 +lemma approx_chain_upper_map:
    10.8 +  assumes "approx_chain a"
    10.9 +  shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))"
   10.10 +  using assms unfolding approx_chain_def
   10.11 +  by (simp add: lub_APP upper_map_ID finite_deflation_upper_map)
   10.12 +
   10.13 +instance upper_pd :: ("domain") bifinite
   10.14 +proof
   10.15 +  show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a"
   10.16 +    using bifinite [where 'a='a]
   10.17 +    by (fast intro!: approx_chain_upper_map)
   10.18 +qed
   10.19 +
   10.20  definition
   10.21    upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
   10.22  where
    11.1 --- a/src/HOL/IsaMakefile	Sun Dec 19 04:06:02 2010 -0800
    11.2 +++ b/src/HOL/IsaMakefile	Sun Dec 19 05:15:31 2010 -0800
    11.3 @@ -1404,6 +1404,7 @@
    11.4    HOLCF/ROOT.ML \
    11.5    HOLCF/Adm.thy \
    11.6    HOLCF/Algebraic.thy \
    11.7 +  HOLCF/Bifinite.thy \
    11.8    HOLCF/Cfun.thy \
    11.9    HOLCF/Compact_Basis.thy \
   11.10    HOLCF/Completion.thy \