move all bifinite class instances to Bifinite.thy
authorhuffman
Sat Oct 09 07:24:49 2010 -0700 (2010-10-09)
changeset 399878c2f449af35a
parent 39986 38677db30cad
child 39988 a4b2971952f4
move all bifinite class instances to Bifinite.thy
src/HOLCF/Bifinite.thy
src/HOLCF/Cprod.thy
src/HOLCF/Lift.thy
src/HOLCF/Representable.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Fri Oct 08 07:39:50 2010 -0700
     1.2 +++ b/src/HOLCF/Bifinite.thy	Sat Oct 09 07:24:49 2010 -0700
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Bifinite domains *}
     1.5  
     1.6  theory Bifinite
     1.7 -imports Algebraic
     1.8 +imports Algebraic Cprod Sprod Ssum Up Lift One Tr
     1.9  begin
    1.10  
    1.11  subsection {* Class of bifinite domains *}
    1.12 @@ -144,7 +144,7 @@
    1.13                     Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
    1.14  qed
    1.15  
    1.16 -subsection {* Instance for universal domain type *}
    1.17 +subsection {* The universal domain is bifinite *}
    1.18  
    1.19  instantiation udom :: bifinite
    1.20  begin
    1.21 @@ -178,7 +178,7 @@
    1.22  
    1.23  end
    1.24  
    1.25 -subsection {* Instance for continuous function space *}
    1.26 +subsection {* Continuous function space is a bifinite domain *}
    1.27  
    1.28  definition
    1.29    cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
    1.30 @@ -237,4 +237,324 @@
    1.31    "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.32  by (rule sfp_cfun_def)
    1.33  
    1.34 +subsection {* Cartesian product is a bifinite domain *}
    1.35 +
    1.36 +definition
    1.37 +  prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
    1.38 +where
    1.39 +  "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.40 +
    1.41 +lemma prod_approx: "approx_chain prod_approx"
    1.42 +proof (rule approx_chain.intro)
    1.43 +  show "chain (\<lambda>i. prod_approx i)"
    1.44 +    unfolding prod_approx_def by simp
    1.45 +  show "(\<Squnion>i. prod_approx i) = ID"
    1.46 +    unfolding prod_approx_def
    1.47 +    by (simp add: lub_distribs cprod_map_ID)
    1.48 +  show "\<And>i. finite_deflation (prod_approx i)"
    1.49 +    unfolding prod_approx_def
    1.50 +    by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
    1.51 +qed
    1.52 +
    1.53 +definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    1.54 +where "prod_sfp = sfp_fun2 prod_approx cprod_map"
    1.55 +
    1.56 +lemma cast_prod_sfp:
    1.57 +  "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
    1.58 +    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
    1.59 +unfolding prod_sfp_def
    1.60 +apply (rule cast_sfp_fun2 [OF prod_approx])
    1.61 +apply (erule (1) finite_deflation_cprod_map)
    1.62 +done
    1.63 +
    1.64 +instantiation prod :: (bifinite, bifinite) bifinite
    1.65 +begin
    1.66 +
    1.67 +definition
    1.68 +  "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
    1.69 +
    1.70 +definition
    1.71 +  "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
    1.72 +
    1.73 +definition
    1.74 +  "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.75 +
    1.76 +instance proof
    1.77 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
    1.78 +    unfolding emb_prod_def prj_prod_def
    1.79 +    using ep_pair_udom [OF prod_approx]
    1.80 +    by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
    1.81 +next
    1.82 +  show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
    1.83 +    unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
    1.84 +    by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
    1.85 +qed
    1.86 +
    1.87  end
    1.88 +
    1.89 +lemma SFP_prod:
    1.90 +  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.91 +by (rule sfp_prod_def)
    1.92 +
    1.93 +subsection {* Strict product is a bifinite domain *}
    1.94 +
    1.95 +definition
    1.96 +  sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    1.97 +where
    1.98 +  "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.99 +
   1.100 +lemma sprod_approx: "approx_chain sprod_approx"
   1.101 +proof (rule approx_chain.intro)
   1.102 +  show "chain (\<lambda>i. sprod_approx i)"
   1.103 +    unfolding sprod_approx_def by simp
   1.104 +  show "(\<Squnion>i. sprod_approx i) = ID"
   1.105 +    unfolding sprod_approx_def
   1.106 +    by (simp add: lub_distribs sprod_map_ID)
   1.107 +  show "\<And>i. finite_deflation (sprod_approx i)"
   1.108 +    unfolding sprod_approx_def
   1.109 +    by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
   1.110 +qed
   1.111 +
   1.112 +definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   1.113 +where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
   1.114 +
   1.115 +lemma cast_sprod_sfp:
   1.116 +  "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
   1.117 +    udom_emb sprod_approx oo
   1.118 +      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
   1.119 +        udom_prj sprod_approx"
   1.120 +unfolding sprod_sfp_def
   1.121 +apply (rule cast_sfp_fun2 [OF sprod_approx])
   1.122 +apply (erule (1) finite_deflation_sprod_map)
   1.123 +done
   1.124 +
   1.125 +instantiation sprod :: (bifinite, bifinite) bifinite
   1.126 +begin
   1.127 +
   1.128 +definition
   1.129 +  "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
   1.130 +
   1.131 +definition
   1.132 +  "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
   1.133 +
   1.134 +definition
   1.135 +  "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   1.136 +
   1.137 +instance proof
   1.138 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   1.139 +    unfolding emb_sprod_def prj_sprod_def
   1.140 +    using ep_pair_udom [OF sprod_approx]
   1.141 +    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
   1.142 +next
   1.143 +  show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
   1.144 +    unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
   1.145 +    by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
   1.146 +qed
   1.147 +
   1.148 +end
   1.149 +
   1.150 +lemma SFP_sprod:
   1.151 +  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   1.152 +by (rule sfp_sprod_def)
   1.153 +
   1.154 +subsection {* Lifted cpo is a bifinite domain *}
   1.155 +
   1.156 +definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
   1.157 +where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
   1.158 +
   1.159 +lemma u_approx: "approx_chain u_approx"
   1.160 +proof (rule approx_chain.intro)
   1.161 +  show "chain (\<lambda>i. u_approx i)"
   1.162 +    unfolding u_approx_def by simp
   1.163 +  show "(\<Squnion>i. u_approx i) = ID"
   1.164 +    unfolding u_approx_def
   1.165 +    by (simp add: lub_distribs u_map_ID)
   1.166 +  show "\<And>i. finite_deflation (u_approx i)"
   1.167 +    unfolding u_approx_def
   1.168 +    by (intro finite_deflation_u_map finite_deflation_udom_approx)
   1.169 +qed
   1.170 +
   1.171 +definition u_sfp :: "sfp \<rightarrow> sfp"
   1.172 +where "u_sfp = sfp_fun1 u_approx u_map"
   1.173 +
   1.174 +lemma cast_u_sfp:
   1.175 +  "cast\<cdot>(u_sfp\<cdot>A) =
   1.176 +    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
   1.177 +unfolding u_sfp_def
   1.178 +apply (rule cast_sfp_fun1 [OF u_approx])
   1.179 +apply (erule finite_deflation_u_map)
   1.180 +done
   1.181 +
   1.182 +instantiation u :: (bifinite) bifinite
   1.183 +begin
   1.184 +
   1.185 +definition
   1.186 +  "emb = udom_emb u_approx oo u_map\<cdot>emb"
   1.187 +
   1.188 +definition
   1.189 +  "prj = u_map\<cdot>prj oo udom_prj u_approx"
   1.190 +
   1.191 +definition
   1.192 +  "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
   1.193 +
   1.194 +instance proof
   1.195 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
   1.196 +    unfolding emb_u_def prj_u_def
   1.197 +    using ep_pair_udom [OF u_approx]
   1.198 +    by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
   1.199 +next
   1.200 +  show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
   1.201 +    unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
   1.202 +    by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
   1.203 +qed
   1.204 +
   1.205 +end
   1.206 +
   1.207 +lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
   1.208 +by (rule sfp_u_def)
   1.209 +
   1.210 +subsection {* Lifted countable types are bifinite domains *}
   1.211 +
   1.212 +definition
   1.213 +  lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
   1.214 +where
   1.215 +  "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
   1.216 +
   1.217 +lemma chain_lift_approx [simp]: "chain lift_approx"
   1.218 +  unfolding lift_approx_def
   1.219 +  by (rule chainI, simp add: FLIFT_mono)
   1.220 +
   1.221 +lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
   1.222 +apply (rule ext_cfun)
   1.223 +apply (simp add: contlub_cfun_fun)
   1.224 +apply (simp add: lift_approx_def)
   1.225 +apply (case_tac x, simp)
   1.226 +apply (rule thelubI)
   1.227 +apply (rule is_lubI)
   1.228 +apply (rule ub_rangeI, simp)
   1.229 +apply (drule ub_rangeD)
   1.230 +apply (erule rev_below_trans)
   1.231 +apply simp
   1.232 +apply (rule lessI)
   1.233 +done
   1.234 +
   1.235 +lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
   1.236 +proof
   1.237 +  fix x
   1.238 +  show "lift_approx i\<cdot>x \<sqsubseteq> x"
   1.239 +    unfolding lift_approx_def
   1.240 +    by (cases x, simp, simp)
   1.241 +  show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
   1.242 +    unfolding lift_approx_def
   1.243 +    by (cases x, simp, simp)
   1.244 +  show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
   1.245 +  proof (rule finite_subset)
   1.246 +    let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
   1.247 +    show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
   1.248 +      unfolding lift_approx_def
   1.249 +      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
   1.250 +    show "finite ?S"
   1.251 +      by (simp add: finite_vimageI)
   1.252 +  qed
   1.253 +qed
   1.254 +
   1.255 +lemma lift_approx: "approx_chain lift_approx"
   1.256 +using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
   1.257 +by (rule approx_chain.intro)
   1.258 +
   1.259 +instantiation lift :: (countable) bifinite
   1.260 +begin
   1.261 +
   1.262 +definition
   1.263 +  "emb = udom_emb lift_approx"
   1.264 +
   1.265 +definition
   1.266 +  "prj = udom_prj lift_approx"
   1.267 +
   1.268 +definition
   1.269 +  "sfp (t::'a lift itself) =
   1.270 +    (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
   1.271 +
   1.272 +instance proof
   1.273 +  show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
   1.274 +    unfolding emb_lift_def prj_lift_def
   1.275 +    by (rule ep_pair_udom [OF lift_approx])
   1.276 +  show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
   1.277 +    unfolding sfp_lift_def
   1.278 +    apply (subst contlub_cfun_arg)
   1.279 +    apply (rule chainI)
   1.280 +    apply (rule sfp.principal_mono)
   1.281 +    apply (simp add: below_fin_defl_def)
   1.282 +    apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
   1.283 +                     ep_pair.finite_deflation_e_d_p [OF ep])
   1.284 +    apply (intro monofun_cfun below_refl)
   1.285 +    apply (rule chainE)
   1.286 +    apply (rule chain_lift_approx)
   1.287 +    apply (subst cast_sfp_principal)
   1.288 +    apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
   1.289 +                     ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
   1.290 +    done
   1.291 +qed
   1.292 +
   1.293 +end
   1.294 +
   1.295 +subsection {* Strict sum is a bifinite domain *}
   1.296 +
   1.297 +definition
   1.298 +  ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
   1.299 +where
   1.300 +  "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   1.301 +
   1.302 +lemma ssum_approx: "approx_chain ssum_approx"
   1.303 +proof (rule approx_chain.intro)
   1.304 +  show "chain (\<lambda>i. ssum_approx i)"
   1.305 +    unfolding ssum_approx_def by simp
   1.306 +  show "(\<Squnion>i. ssum_approx i) = ID"
   1.307 +    unfolding ssum_approx_def
   1.308 +    by (simp add: lub_distribs ssum_map_ID)
   1.309 +  show "\<And>i. finite_deflation (ssum_approx i)"
   1.310 +    unfolding ssum_approx_def
   1.311 +    by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
   1.312 +qed
   1.313 +
   1.314 +definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   1.315 +where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
   1.316 +
   1.317 +lemma cast_ssum_sfp:
   1.318 +  "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
   1.319 +    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
   1.320 +unfolding ssum_sfp_def
   1.321 +apply (rule cast_sfp_fun2 [OF ssum_approx])
   1.322 +apply (erule (1) finite_deflation_ssum_map)
   1.323 +done
   1.324 +
   1.325 +instantiation ssum :: (bifinite, bifinite) bifinite
   1.326 +begin
   1.327 +
   1.328 +definition
   1.329 +  "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
   1.330 +
   1.331 +definition
   1.332 +  "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
   1.333 +
   1.334 +definition
   1.335 +  "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   1.336 +
   1.337 +instance proof
   1.338 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   1.339 +    unfolding emb_ssum_def prj_ssum_def
   1.340 +    using ep_pair_udom [OF ssum_approx]
   1.341 +    by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
   1.342 +next
   1.343 +  show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
   1.344 +    unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
   1.345 +    by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
   1.346 +qed
   1.347 +
   1.348 +end
   1.349 +
   1.350 +lemma SFP_ssum:
   1.351 +  "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   1.352 +by (rule sfp_ssum_def)
   1.353 +
   1.354 +end
     2.1 --- a/src/HOLCF/Cprod.thy	Fri Oct 08 07:39:50 2010 -0700
     2.2 +++ b/src/HOLCF/Cprod.thy	Sat Oct 09 07:24:49 2010 -0700
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* The cpo of cartesian products *}
     2.5  
     2.6  theory Cprod
     2.7 -imports Bifinite
     2.8 +imports Deflation
     2.9  begin
    2.10  
    2.11  default_sort cpo
    2.12 @@ -97,63 +97,4 @@
    2.13      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    2.14  qed
    2.15  
    2.16 -subsection {* Cartesian product is a bifinite domain *}
    2.17 -
    2.18 -definition
    2.19 -  prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
    2.20 -where
    2.21 -  "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    2.22 -
    2.23 -lemma prod_approx: "approx_chain prod_approx"
    2.24 -proof (rule approx_chain.intro)
    2.25 -  show "chain (\<lambda>i. prod_approx i)"
    2.26 -    unfolding prod_approx_def by simp
    2.27 -  show "(\<Squnion>i. prod_approx i) = ID"
    2.28 -    unfolding prod_approx_def
    2.29 -    by (simp add: lub_distribs cprod_map_ID)
    2.30 -  show "\<And>i. finite_deflation (prod_approx i)"
    2.31 -    unfolding prod_approx_def
    2.32 -    by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
    2.33 -qed
    2.34 -
    2.35 -definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    2.36 -where "prod_sfp = sfp_fun2 prod_approx cprod_map"
    2.37 -
    2.38 -lemma cast_prod_sfp:
    2.39 -  "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
    2.40 -    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
    2.41 -unfolding prod_sfp_def
    2.42 -apply (rule cast_sfp_fun2 [OF prod_approx])
    2.43 -apply (erule (1) finite_deflation_cprod_map)
    2.44 -done
    2.45 -
    2.46 -instantiation prod :: (bifinite, bifinite) bifinite
    2.47 -begin
    2.48 -
    2.49 -definition
    2.50 -  "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
    2.51 -
    2.52 -definition
    2.53 -  "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
    2.54 -
    2.55 -definition
    2.56 -  "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    2.57 -
    2.58 -instance proof
    2.59 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
    2.60 -    unfolding emb_prod_def prj_prod_def
    2.61 -    using ep_pair_udom [OF prod_approx]
    2.62 -    by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
    2.63 -next
    2.64 -  show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
    2.65 -    unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
    2.66 -    by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
    2.67 -qed
    2.68 -
    2.69  end
    2.70 -
    2.71 -lemma SFP_prod:
    2.72 -  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    2.73 -by (rule sfp_prod_def)
    2.74 -
    2.75 -end
     3.1 --- a/src/HOLCF/Lift.thy	Fri Oct 08 07:39:50 2010 -0700
     3.2 +++ b/src/HOLCF/Lift.thy	Sat Oct 09 07:24:49 2010 -0700
     3.3 @@ -170,90 +170,4 @@
     3.4  lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
     3.5  by (cases x, simp_all)
     3.6  
     3.7 -
     3.8 -subsection {* Lifted countable types are bifinite domains *}
     3.9 -
    3.10 -definition
    3.11 -  lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
    3.12 -where
    3.13 -  "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
    3.14 -
    3.15 -lemma chain_lift_approx [simp]: "chain lift_approx"
    3.16 -  unfolding lift_approx_def
    3.17 -  by (rule chainI, simp add: FLIFT_mono)
    3.18 -
    3.19 -lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
    3.20 -apply (rule ext_cfun)
    3.21 -apply (simp add: contlub_cfun_fun)
    3.22 -apply (simp add: lift_approx_def)
    3.23 -apply (case_tac x, simp)
    3.24 -apply (rule thelubI)
    3.25 -apply (rule is_lubI)
    3.26 -apply (rule ub_rangeI, simp)
    3.27 -apply (drule ub_rangeD)
    3.28 -apply (erule rev_below_trans)
    3.29 -apply simp
    3.30 -apply (rule lessI)
    3.31 -done
    3.32 -
    3.33 -lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
    3.34 -proof
    3.35 -  fix x
    3.36 -  show "lift_approx i\<cdot>x \<sqsubseteq> x"
    3.37 -    unfolding lift_approx_def
    3.38 -    by (cases x, simp, simp)
    3.39 -  show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
    3.40 -    unfolding lift_approx_def
    3.41 -    by (cases x, simp, simp)
    3.42 -  show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
    3.43 -  proof (rule finite_subset)
    3.44 -    let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
    3.45 -    show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
    3.46 -      unfolding lift_approx_def
    3.47 -      by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
    3.48 -    show "finite ?S"
    3.49 -      by (simp add: finite_vimageI)
    3.50 -  qed
    3.51 -qed
    3.52 -
    3.53 -lemma lift_approx: "approx_chain lift_approx"
    3.54 -using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
    3.55 -by (rule approx_chain.intro)
    3.56 -
    3.57 -instantiation lift :: (countable) bifinite
    3.58 -begin
    3.59 -
    3.60 -definition
    3.61 -  "emb = udom_emb lift_approx"
    3.62 -
    3.63 -definition
    3.64 -  "prj = udom_prj lift_approx"
    3.65 -
    3.66 -definition
    3.67 -  "sfp (t::'a lift itself) =
    3.68 -    (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
    3.69 -
    3.70 -instance proof
    3.71 -  show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
    3.72 -    unfolding emb_lift_def prj_lift_def
    3.73 -    by (rule ep_pair_udom [OF lift_approx])
    3.74 -  show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
    3.75 -    unfolding sfp_lift_def
    3.76 -    apply (subst contlub_cfun_arg)
    3.77 -    apply (rule chainI)
    3.78 -    apply (rule sfp.principal_mono)
    3.79 -    apply (simp add: below_fin_defl_def)
    3.80 -    apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
    3.81 -                     ep_pair.finite_deflation_e_d_p [OF ep])
    3.82 -    apply (intro monofun_cfun below_refl)
    3.83 -    apply (rule chainE)
    3.84 -    apply (rule chain_lift_approx)
    3.85 -    apply (subst cast_sfp_principal)
    3.86 -    apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
    3.87 -                     ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
    3.88 -    done
    3.89 -qed
    3.90 -
    3.91  end
    3.92 -
    3.93 -end
     4.1 --- a/src/HOLCF/Representable.thy	Fri Oct 08 07:39:50 2010 -0700
     4.2 +++ b/src/HOLCF/Representable.thy	Sat Oct 09 07:24:49 2010 -0700
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Representable Types *}
     4.5  
     4.6  theory Representable
     4.7 -imports Algebraic Universal Ssum One Fixrec Domain_Aux
     4.8 +imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
     4.9  uses
    4.10    ("Tools/repdef.ML")
    4.11    ("Tools/Domain/domain_isomorphism.ML")
     5.1 --- a/src/HOLCF/Sprod.thy	Fri Oct 08 07:39:50 2010 -0700
     5.2 +++ b/src/HOLCF/Sprod.thy	Sat Oct 09 07:24:49 2010 -0700
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* The type of strict products *}
     5.5  
     5.6  theory Sprod
     5.7 -imports Bifinite
     5.8 +imports Deflation
     5.9  begin
    5.10  
    5.11  default_sort pcpo
    5.12 @@ -310,65 +310,4 @@
    5.13      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    5.14  qed
    5.15  
    5.16 -subsection {* Strict product is a bifinite domain *}
    5.17 -
    5.18 -definition
    5.19 -  sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    5.20 -where
    5.21 -  "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    5.22 -
    5.23 -lemma sprod_approx: "approx_chain sprod_approx"
    5.24 -proof (rule approx_chain.intro)
    5.25 -  show "chain (\<lambda>i. sprod_approx i)"
    5.26 -    unfolding sprod_approx_def by simp
    5.27 -  show "(\<Squnion>i. sprod_approx i) = ID"
    5.28 -    unfolding sprod_approx_def
    5.29 -    by (simp add: lub_distribs sprod_map_ID)
    5.30 -  show "\<And>i. finite_deflation (sprod_approx i)"
    5.31 -    unfolding sprod_approx_def
    5.32 -    by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
    5.33 -qed
    5.34 -
    5.35 -definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    5.36 -where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
    5.37 -
    5.38 -lemma cast_sprod_sfp:
    5.39 -  "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
    5.40 -    udom_emb sprod_approx oo
    5.41 -      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
    5.42 -        udom_prj sprod_approx"
    5.43 -unfolding sprod_sfp_def
    5.44 -apply (rule cast_sfp_fun2 [OF sprod_approx])
    5.45 -apply (erule (1) finite_deflation_sprod_map)
    5.46 -done
    5.47 -
    5.48 -instantiation sprod :: (bifinite, bifinite) bifinite
    5.49 -begin
    5.50 -
    5.51 -definition
    5.52 -  "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
    5.53 -
    5.54 -definition
    5.55 -  "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
    5.56 -
    5.57 -definition
    5.58 -  "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    5.59 -
    5.60 -instance proof
    5.61 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    5.62 -    unfolding emb_sprod_def prj_sprod_def
    5.63 -    using ep_pair_udom [OF sprod_approx]
    5.64 -    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
    5.65 -next
    5.66 -  show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    5.67 -    unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
    5.68 -    by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
    5.69 -qed
    5.70 -
    5.71  end
    5.72 -
    5.73 -lemma SFP_sprod:
    5.74 -  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    5.75 -by (rule sfp_sprod_def)
    5.76 -
    5.77 -end
     6.1 --- a/src/HOLCF/Ssum.thy	Fri Oct 08 07:39:50 2010 -0700
     6.2 +++ b/src/HOLCF/Ssum.thy	Sat Oct 09 07:24:49 2010 -0700
     6.3 @@ -295,63 +295,4 @@
     6.4      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
     6.5  qed
     6.6  
     6.7 -subsection {* Strict sum is a bifinite domain *}
     6.8 -
     6.9 -definition
    6.10 -  ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
    6.11 -where
    6.12 -  "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    6.13 -
    6.14 -lemma ssum_approx: "approx_chain ssum_approx"
    6.15 -proof (rule approx_chain.intro)
    6.16 -  show "chain (\<lambda>i. ssum_approx i)"
    6.17 -    unfolding ssum_approx_def by simp
    6.18 -  show "(\<Squnion>i. ssum_approx i) = ID"
    6.19 -    unfolding ssum_approx_def
    6.20 -    by (simp add: lub_distribs ssum_map_ID)
    6.21 -  show "\<And>i. finite_deflation (ssum_approx i)"
    6.22 -    unfolding ssum_approx_def
    6.23 -    by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
    6.24 -qed
    6.25 -
    6.26 -definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    6.27 -where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
    6.28 -
    6.29 -lemma cast_ssum_sfp:
    6.30 -  "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
    6.31 -    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
    6.32 -unfolding ssum_sfp_def
    6.33 -apply (rule cast_sfp_fun2 [OF ssum_approx])
    6.34 -apply (erule (1) finite_deflation_ssum_map)
    6.35 -done
    6.36 -
    6.37 -instantiation ssum :: (bifinite, bifinite) bifinite
    6.38 -begin
    6.39 -
    6.40 -definition
    6.41 -  "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
    6.42 -
    6.43 -definition
    6.44 -  "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
    6.45 -
    6.46 -definition
    6.47 -  "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    6.48 -
    6.49 -instance proof
    6.50 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
    6.51 -    unfolding emb_ssum_def prj_ssum_def
    6.52 -    using ep_pair_udom [OF ssum_approx]
    6.53 -    by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
    6.54 -next
    6.55 -  show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
    6.56 -    unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
    6.57 -    by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
    6.58 -qed
    6.59 -
    6.60  end
    6.61 -
    6.62 -lemma SFP_ssum:
    6.63 -  "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    6.64 -by (rule sfp_ssum_def)
    6.65 -
    6.66 -end
     7.1 --- a/src/HOLCF/Up.thy	Fri Oct 08 07:39:50 2010 -0700
     7.2 +++ b/src/HOLCF/Up.thy	Sat Oct 09 07:24:49 2010 -0700
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* The type of lifted values *}
     7.5  
     7.6  theory Up
     7.7 -imports Bifinite
     7.8 +imports Deflation
     7.9  begin
    7.10  
    7.11  default_sort cpo
    7.12 @@ -332,60 +332,4 @@
    7.13      by (rule finite_subset, simp add: d.finite_fixes)
    7.14  qed
    7.15  
    7.16 -subsection {* Lifted cpo is a bifinite domain *}
    7.17 -
    7.18 -definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
    7.19 -where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
    7.20 -
    7.21 -lemma u_approx: "approx_chain u_approx"
    7.22 -proof (rule approx_chain.intro)
    7.23 -  show "chain (\<lambda>i. u_approx i)"
    7.24 -    unfolding u_approx_def by simp
    7.25 -  show "(\<Squnion>i. u_approx i) = ID"
    7.26 -    unfolding u_approx_def
    7.27 -    by (simp add: lub_distribs u_map_ID)
    7.28 -  show "\<And>i. finite_deflation (u_approx i)"
    7.29 -    unfolding u_approx_def
    7.30 -    by (intro finite_deflation_u_map finite_deflation_udom_approx)
    7.31 -qed
    7.32 -
    7.33 -definition u_sfp :: "sfp \<rightarrow> sfp"
    7.34 -where "u_sfp = sfp_fun1 u_approx u_map"
    7.35 -
    7.36 -lemma cast_u_sfp:
    7.37 -  "cast\<cdot>(u_sfp\<cdot>A) =
    7.38 -    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
    7.39 -unfolding u_sfp_def
    7.40 -apply (rule cast_sfp_fun1 [OF u_approx])
    7.41 -apply (erule finite_deflation_u_map)
    7.42 -done
    7.43 -
    7.44 -instantiation u :: (bifinite) bifinite
    7.45 -begin
    7.46 -
    7.47 -definition
    7.48 -  "emb = udom_emb u_approx oo u_map\<cdot>emb"
    7.49 -
    7.50 -definition
    7.51 -  "prj = u_map\<cdot>prj oo udom_prj u_approx"
    7.52 -
    7.53 -definition
    7.54 -  "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
    7.55 -
    7.56 -instance proof
    7.57 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
    7.58 -    unfolding emb_u_def prj_u_def
    7.59 -    using ep_pair_udom [OF u_approx]
    7.60 -    by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
    7.61 -next
    7.62 -  show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
    7.63 -    unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
    7.64 -    by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
    7.65 -qed
    7.66 -
    7.67  end
    7.68 -
    7.69 -lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
    7.70 -by (rule sfp_u_def)
    7.71 -
    7.72 -end