src/HOL/HOLCF/Bifinite.thy
changeset 41286 3d7685a4a5ff
child 41297 01b2de947cff
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
     1.3 @@ -0,0 +1,275 @@
     1.4 +(*  Title:      HOLCF/Bifinite.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Profinite and bifinite cpos *}
     1.9 +
    1.10 +theory Bifinite
    1.11 +imports Map_Functions Countable
    1.12 +begin
    1.13 +
    1.14 +default_sort cpo
    1.15 +
    1.16 +subsection {* Chains of finite deflations *}
    1.17 +
    1.18 +locale approx_chain =
    1.19 +  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
    1.20 +  assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
    1.21 +  assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"
    1.22 +  assumes finite_deflation_approx [simp]: "\<And>i. finite_deflation (approx i)"
    1.23 +begin
    1.24 +
    1.25 +lemma deflation_approx: "deflation (approx i)"
    1.26 +using finite_deflation_approx by (rule finite_deflation_imp_deflation)
    1.27 +
    1.28 +lemma approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.29 +using deflation_approx by (rule deflation.idem)
    1.30 +
    1.31 +lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
    1.32 +using deflation_approx by (rule deflation.below)
    1.33 +
    1.34 +lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
    1.35 +apply (rule finite_deflation.finite_range)
    1.36 +apply (rule finite_deflation_approx)
    1.37 +done
    1.38 +
    1.39 +lemma compact_approx: "compact (approx n\<cdot>x)"
    1.40 +apply (rule finite_deflation.compact)
    1.41 +apply (rule finite_deflation_approx)
    1.42 +done
    1.43 +
    1.44 +lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
    1.45 +by (rule admD2, simp_all)
    1.46 +
    1.47 +end
    1.48 +
    1.49 +subsection {* Omega-profinite and bifinite domains *}
    1.50 +
    1.51 +class bifinite = pcpo +
    1.52 +  assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
    1.53 +
    1.54 +class profinite = cpo +
    1.55 +  assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
    1.56 +
    1.57 +subsection {* Building approx chains *}
    1.58 +
    1.59 +lemma approx_chain_iso:
    1.60 +  assumes a: "approx_chain a"
    1.61 +  assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
    1.62 +  assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"
    1.63 +  shows "approx_chain (\<lambda>i. f oo a i oo g)"
    1.64 +proof -
    1.65 +  have 1: "f oo g = ID" by (simp add: cfun_eqI)
    1.66 +  have 2: "ep_pair f g" by (simp add: ep_pair_def)
    1.67 +  from 1 2 show ?thesis
    1.68 +    using a unfolding approx_chain_def
    1.69 +    by (simp add: lub_APP ep_pair.finite_deflation_e_d_p)
    1.70 +qed
    1.71 +
    1.72 +lemma approx_chain_u_map:
    1.73 +  assumes "approx_chain a"
    1.74 +  shows "approx_chain (\<lambda>i. u_map\<cdot>(a i))"
    1.75 +  using assms unfolding approx_chain_def
    1.76 +  by (simp add: lub_APP u_map_ID finite_deflation_u_map)
    1.77 +
    1.78 +lemma approx_chain_sfun_map:
    1.79 +  assumes "approx_chain a" and "approx_chain b"
    1.80 +  shows "approx_chain (\<lambda>i. sfun_map\<cdot>(a i)\<cdot>(b i))"
    1.81 +  using assms unfolding approx_chain_def
    1.82 +  by (simp add: lub_APP sfun_map_ID finite_deflation_sfun_map)
    1.83 +
    1.84 +lemma approx_chain_sprod_map:
    1.85 +  assumes "approx_chain a" and "approx_chain b"
    1.86 +  shows "approx_chain (\<lambda>i. sprod_map\<cdot>(a i)\<cdot>(b i))"
    1.87 +  using assms unfolding approx_chain_def
    1.88 +  by (simp add: lub_APP sprod_map_ID finite_deflation_sprod_map)
    1.89 +
    1.90 +lemma approx_chain_ssum_map:
    1.91 +  assumes "approx_chain a" and "approx_chain b"
    1.92 +  shows "approx_chain (\<lambda>i. ssum_map\<cdot>(a i)\<cdot>(b i))"
    1.93 +  using assms unfolding approx_chain_def
    1.94 +  by (simp add: lub_APP ssum_map_ID finite_deflation_ssum_map)
    1.95 +
    1.96 +lemma approx_chain_cfun_map:
    1.97 +  assumes "approx_chain a" and "approx_chain b"
    1.98 +  shows "approx_chain (\<lambda>i. cfun_map\<cdot>(a i)\<cdot>(b i))"
    1.99 +  using assms unfolding approx_chain_def
   1.100 +  by (simp add: lub_APP cfun_map_ID finite_deflation_cfun_map)
   1.101 +
   1.102 +lemma approx_chain_cprod_map:
   1.103 +  assumes "approx_chain a" and "approx_chain b"
   1.104 +  shows "approx_chain (\<lambda>i. cprod_map\<cdot>(a i)\<cdot>(b i))"
   1.105 +  using assms unfolding approx_chain_def
   1.106 +  by (simp add: lub_APP cprod_map_ID finite_deflation_cprod_map)
   1.107 +
   1.108 +text {* Approx chains for countable discrete types. *}
   1.109 +
   1.110 +definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   1.111 +  where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
   1.112 +
   1.113 +lemma chain_discr_approx [simp]: "chain discr_approx"
   1.114 +unfolding discr_approx_def
   1.115 +by (rule chainI, simp add: monofun_cfun monofun_LAM)
   1.116 +
   1.117 +lemma lub_discr_approx [simp]: "(\<Squnion>i. discr_approx i) = ID"
   1.118 +apply (rule cfun_eqI)
   1.119 +apply (simp add: contlub_cfun_fun)
   1.120 +apply (simp add: discr_approx_def)
   1.121 +apply (case_tac x, simp)
   1.122 +apply (rule lub_eqI)
   1.123 +apply (rule is_lubI)
   1.124 +apply (rule ub_rangeI, simp)
   1.125 +apply (drule ub_rangeD)
   1.126 +apply (erule rev_below_trans)
   1.127 +apply simp
   1.128 +apply (rule lessI)
   1.129 +done
   1.130 +
   1.131 +lemma inj_on_undiscr [simp]: "inj_on undiscr A"
   1.132 +using Discr_undiscr by (rule inj_on_inverseI)
   1.133 +
   1.134 +lemma finite_deflation_discr_approx: "finite_deflation (discr_approx i)"
   1.135 +proof
   1.136 +  fix x :: "'a discr u"
   1.137 +  show "discr_approx i\<cdot>x \<sqsubseteq> x"
   1.138 +    unfolding discr_approx_def
   1.139 +    by (cases x, simp, simp)
   1.140 +  show "discr_approx i\<cdot>(discr_approx i\<cdot>x) = discr_approx i\<cdot>x"
   1.141 +    unfolding discr_approx_def
   1.142 +    by (cases x, simp, simp)
   1.143 +  show "finite {x::'a discr u. discr_approx i\<cdot>x = x}"
   1.144 +  proof (rule finite_subset)
   1.145 +    let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
   1.146 +    show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
   1.147 +      unfolding discr_approx_def
   1.148 +      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
   1.149 +    show "finite ?S"
   1.150 +      by (simp add: finite_vimageI)
   1.151 +  qed
   1.152 +qed
   1.153 +
   1.154 +lemma discr_approx: "approx_chain discr_approx"
   1.155 +using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
   1.156 +by (rule approx_chain.intro)
   1.157 +
   1.158 +subsection {* Class instance proofs *}
   1.159 +
   1.160 +instance bifinite \<subseteq> profinite
   1.161 +proof
   1.162 +  show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
   1.163 +    using bifinite [where 'a='a]
   1.164 +    by (fast intro!: approx_chain_u_map)
   1.165 +qed
   1.166 +
   1.167 +instance u :: (profinite) bifinite
   1.168 +  by default (rule profinite)
   1.169 +
   1.170 +text {*
   1.171 +  Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
   1.172 +*}
   1.173 +
   1.174 +definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
   1.175 +
   1.176 +definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
   1.177 +
   1.178 +lemma decode_encode_cfun [simp]: "decode_cfun\<cdot>(encode_cfun\<cdot>x) = x"
   1.179 +unfolding encode_cfun_def decode_cfun_def
   1.180 +by (simp add: eta_cfun)
   1.181 +
   1.182 +lemma encode_decode_cfun [simp]: "encode_cfun\<cdot>(decode_cfun\<cdot>y) = y"
   1.183 +unfolding encode_cfun_def decode_cfun_def
   1.184 +apply (simp add: sfun_eq_iff strictify_cancel)
   1.185 +apply (rule cfun_eqI, case_tac x, simp_all)
   1.186 +done
   1.187 +
   1.188 +instance cfun :: (profinite, bifinite) bifinite
   1.189 +proof
   1.190 +  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
   1.191 +    using profinite ..
   1.192 +  obtain b :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where b: "approx_chain b"
   1.193 +    using bifinite ..
   1.194 +  have "approx_chain (\<lambda>i. decode_cfun oo sfun_map\<cdot>(a i)\<cdot>(b i) oo encode_cfun)"
   1.195 +    using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
   1.196 +  thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
   1.197 +    by - (rule exI)
   1.198 +qed
   1.199 +
   1.200 +text {*
   1.201 +  Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
   1.202 +*}
   1.203 +
   1.204 +definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
   1.205 +
   1.206 +definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"
   1.207 +
   1.208 +lemma decode_encode_prod_u [simp]: "decode_prod_u\<cdot>(encode_prod_u\<cdot>x) = x"
   1.209 +unfolding encode_prod_u_def decode_prod_u_def
   1.210 +by (case_tac x, simp, rename_tac y, case_tac y, simp)
   1.211 +
   1.212 +lemma encode_decode_prod_u [simp]: "encode_prod_u\<cdot>(decode_prod_u\<cdot>y) = y"
   1.213 +unfolding encode_prod_u_def decode_prod_u_def
   1.214 +apply (case_tac y, simp, rename_tac a b)
   1.215 +apply (case_tac a, simp, case_tac b, simp, simp)
   1.216 +done
   1.217 +
   1.218 +instance prod :: (profinite, profinite) profinite
   1.219 +proof
   1.220 +  obtain a :: "nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>" where a: "approx_chain a"
   1.221 +    using profinite ..
   1.222 +  obtain b :: "nat \<Rightarrow> 'b\<^sub>\<bottom> \<rightarrow> 'b\<^sub>\<bottom>" where b: "approx_chain b"
   1.223 +    using profinite ..
   1.224 +  have "approx_chain (\<lambda>i. decode_prod_u oo sprod_map\<cdot>(a i)\<cdot>(b i) oo encode_prod_u)"
   1.225 +    using a b by (simp add: approx_chain_iso approx_chain_sprod_map)
   1.226 +  thus "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>). approx_chain a"
   1.227 +    by - (rule exI)
   1.228 +qed
   1.229 +
   1.230 +instance prod :: (bifinite, bifinite) bifinite
   1.231 +proof
   1.232 +  show "\<exists>(a::nat \<Rightarrow> ('a \<times> 'b) \<rightarrow> ('a \<times> 'b)). approx_chain a"
   1.233 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   1.234 +    by (fast intro!: approx_chain_cprod_map)
   1.235 +qed
   1.236 +
   1.237 +instance sfun :: (bifinite, bifinite) bifinite
   1.238 +proof
   1.239 +  show "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow>! 'b) \<rightarrow> ('a \<rightarrow>! 'b)). approx_chain a"
   1.240 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   1.241 +    by (fast intro!: approx_chain_sfun_map)
   1.242 +qed
   1.243 +
   1.244 +instance sprod :: (bifinite, bifinite) bifinite
   1.245 +proof
   1.246 +  show "\<exists>(a::nat \<Rightarrow> ('a \<otimes> 'b) \<rightarrow> ('a \<otimes> 'b)). approx_chain a"
   1.247 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   1.248 +    by (fast intro!: approx_chain_sprod_map)
   1.249 +qed
   1.250 +
   1.251 +instance ssum :: (bifinite, bifinite) bifinite
   1.252 +proof
   1.253 +  show "\<exists>(a::nat \<Rightarrow> ('a \<oplus> 'b) \<rightarrow> ('a \<oplus> 'b)). approx_chain a"
   1.254 +    using bifinite [where 'a='a] and bifinite [where 'a='b]
   1.255 +    by (fast intro!: approx_chain_ssum_map)
   1.256 +qed
   1.257 +
   1.258 +lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
   1.259 +by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
   1.260 +
   1.261 +instance unit :: bifinite
   1.262 +  by default (fast intro!: approx_chain_unit)
   1.263 +
   1.264 +instance discr :: (countable) profinite
   1.265 +  by default (fast intro!: discr_approx)
   1.266 +
   1.267 +instance lift :: (countable) bifinite
   1.268 +proof
   1.269 +  note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
   1.270 +  obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"
   1.271 +    using profinite ..
   1.272 +  hence "approx_chain (\<lambda>i. (\<Lambda> y. Abs_lift y) oo a i oo (\<Lambda> x. Rep_lift x))"
   1.273 +    by (rule approx_chain_iso) simp_all
   1.274 +  thus "\<exists>(a::nat \<Rightarrow> 'a lift \<rightarrow> 'a lift). approx_chain a"
   1.275 +    by - (rule exI)
   1.276 +qed
   1.277 +
   1.278 +end