1.1 --- a/src/HOLCF/Bifinite.thy	Mon Nov 08 05:07:18 2010 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Mon Nov 08 06:58:09 2010 -0800
     1.3 @@ -71,6 +71,58 @@
     1.4    show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
     1.5  qed
     1.6  
     1.7 +subsection {* Chains of approx functions *}
     1.8 +
     1.9 +definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
    1.10 +  where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
    1.11 +
    1.12 +definition cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
    1.13 +  where "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.14 +
    1.15 +definition prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
    1.16 +  where "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.17 +
    1.18 +definition sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    1.19 +  where "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.20 +
    1.21 +definition ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
    1.22 +  where "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.23 +
    1.24 +lemma approx_chain_lemma1:
    1.25 +  assumes "m\<cdot>ID = ID"
    1.26 +  assumes "\<And>d. finite_deflation d \<Longrightarrow> finite_deflation (m\<cdot>d)"
    1.27 +  shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i))"
    1.28 +by (rule approx_chain.intro)
    1.29 +   (simp_all add: lub_distribs finite_deflation_udom_approx assms)
    1.30 +
    1.31 +lemma approx_chain_lemma2:
    1.32 +  assumes "m\<cdot>ID\<cdot>ID = ID"
    1.33 +  assumes "\<And>a b. \<lbrakk>finite_deflation a; finite_deflation b\<rbrakk>
    1.34 +    \<Longrightarrow> finite_deflation (m\<cdot>a\<cdot>b)"
    1.35 +  shows "approx_chain (\<lambda>i. m\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.36 +by (rule approx_chain.intro)
    1.37 +   (simp_all add: lub_distribs finite_deflation_udom_approx assms)
    1.38 +
    1.39 +lemma u_approx: "approx_chain u_approx"
    1.40 +using u_map_ID finite_deflation_u_map
    1.41 +unfolding u_approx_def by (rule approx_chain_lemma1)
    1.42 +
    1.43 +lemma cfun_approx: "approx_chain cfun_approx"
    1.44 +using cfun_map_ID finite_deflation_cfun_map
    1.45 +unfolding cfun_approx_def by (rule approx_chain_lemma2)
    1.46 +
    1.47 +lemma prod_approx: "approx_chain prod_approx"
    1.48 +using cprod_map_ID finite_deflation_cprod_map
    1.49 +unfolding prod_approx_def by (rule approx_chain_lemma2)
    1.50 +
    1.51 +lemma sprod_approx: "approx_chain sprod_approx"
    1.52 +using sprod_map_ID finite_deflation_sprod_map
    1.53 +unfolding sprod_approx_def by (rule approx_chain_lemma2)
    1.54 +
    1.55 +lemma ssum_approx: "approx_chain ssum_approx"
    1.56 +using ssum_map_ID finite_deflation_ssum_map
    1.57 +unfolding ssum_approx_def by (rule approx_chain_lemma2)
    1.58 +
    1.59  subsection {* Type combinators *}
    1.60  
    1.61  definition
    1.62 @@ -144,6 +196,53 @@
    1.63                     Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
    1.64  qed
    1.65  
    1.66 +definition u_defl :: "defl \<rightarrow> defl"
    1.67 +  where "u_defl = defl_fun1 u_approx u_map"
    1.68 +
    1.69 +definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    1.70 +  where "cfun_defl = defl_fun2 cfun_approx cfun_map"
    1.71 +
    1.72 +definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    1.73 +  where "prod_defl = defl_fun2 prod_approx cprod_map"
    1.74 +
    1.75 +definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    1.76 +  where "sprod_defl = defl_fun2 sprod_approx sprod_map"
    1.77 +
    1.78 +definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
    1.79 +where "ssum_defl = defl_fun2 ssum_approx ssum_map"
    1.80 +
    1.81 +lemma cast_u_defl:
    1.82 +  "cast\<cdot>(u_defl\<cdot>A) =
    1.83 +    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
    1.84 +using u_approx finite_deflation_u_map
    1.85 +unfolding u_defl_def by (rule cast_defl_fun1)
    1.86 +
    1.87 +lemma cast_cfun_defl:
    1.88 +  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
    1.89 +    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
    1.90 +using cfun_approx finite_deflation_cfun_map
    1.91 +unfolding cfun_defl_def by (rule cast_defl_fun2)
    1.92 +
    1.93 +lemma cast_prod_defl:
    1.94 +  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
    1.95 +    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
    1.96 +using prod_approx finite_deflation_cprod_map
    1.97 +unfolding prod_defl_def by (rule cast_defl_fun2)
    1.98 +
    1.99 +lemma cast_sprod_defl:
   1.100 +  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
   1.101 +    udom_emb sprod_approx oo
   1.102 +      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
   1.103 +        udom_prj sprod_approx"
   1.104 +using sprod_approx finite_deflation_sprod_map
   1.105 +unfolding sprod_defl_def by (rule cast_defl_fun2)
   1.106 +
   1.107 +lemma cast_ssum_defl:
   1.108 +  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
   1.109 +    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
   1.110 +using ssum_approx finite_deflation_ssum_map
   1.111 +unfolding ssum_defl_def by (rule cast_defl_fun2)
   1.112 +
   1.113  subsection {* The universal domain is bifinite *}
   1.114  
   1.115  instantiation udom :: bifinite
   1.116 @@ -161,7 +260,6 @@
   1.117  instance proof
   1.118    show "ep_pair emb (prj :: udom \<rightarrow> udom)"
   1.119      by (simp add: ep_pair.intro)
   1.120 -next
   1.121    show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
   1.122      unfolding defl_udom_def
   1.123      apply (subst contlub_cfun_arg)
   1.124 @@ -180,34 +278,6 @@
   1.125  
   1.126  subsection {* Continuous function space is a bifinite domain *}
   1.127  
   1.128 -definition
   1.129 -  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
   1.130 -where
   1.131 -  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   1.132 -
   1.133 -lemma cfun_approx: "approx_chain cfun_approx"
   1.134 -proof (rule approx_chain.intro)
   1.135 -  show "chain (\<lambda>i. cfun_approx i)"
   1.136 -    unfolding cfun_approx_def by simp
   1.137 -  show "(\<Squnion>i. cfun_approx i) = ID"
   1.138 -    unfolding cfun_approx_def
   1.139 -    by (simp add: lub_distribs cfun_map_ID)
   1.140 -  show "\<And>i. finite_deflation (cfun_approx i)"
   1.141 -    unfolding cfun_approx_def
   1.142 -    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
   1.143 -qed
   1.144 -
   1.145 -definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   1.146 -where "cfun_defl = defl_fun2 cfun_approx cfun_map"
   1.147 -
   1.148 -lemma cast_cfun_defl:
   1.149 -  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) =
   1.150 -    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
   1.151 -unfolding cfun_defl_def
   1.152 -apply (rule cast_defl_fun2 [OF cfun_approx])
   1.153 -apply (erule (1) finite_deflation_cfun_map)
   1.154 -done
   1.155 -
   1.156  instantiation cfun :: (bifinite, bifinite) bifinite
   1.157  begin
   1.158  
   1.159 @@ -239,34 +309,6 @@
   1.160  
   1.161  subsection {* Cartesian product is a bifinite domain *}
   1.162  
   1.163 -definition
   1.164 -  prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
   1.165 -where
   1.166 -  "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   1.167 -
   1.168 -lemma prod_approx: "approx_chain prod_approx"
   1.169 -proof (rule approx_chain.intro)
   1.170 -  show "chain (\<lambda>i. prod_approx i)"
   1.171 -    unfolding prod_approx_def by simp
   1.172 -  show "(\<Squnion>i. prod_approx i) = ID"
   1.173 -    unfolding prod_approx_def
   1.174 -    by (simp add: lub_distribs cprod_map_ID)
   1.175 -  show "\<And>i. finite_deflation (prod_approx i)"
   1.176 -    unfolding prod_approx_def
   1.177 -    by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
   1.178 -qed
   1.179 -
   1.180 -definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   1.181 -where "prod_defl = defl_fun2 prod_approx cprod_map"
   1.182 -
   1.183 -lemma cast_prod_defl:
   1.184 -  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo
   1.185 -    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
   1.186 -unfolding prod_defl_def
   1.187 -apply (rule cast_defl_fun2 [OF prod_approx])
   1.188 -apply (erule (1) finite_deflation_cprod_map)
   1.189 -done
   1.190 -
   1.191  instantiation prod :: (bifinite, bifinite) bifinite
   1.192  begin
   1.193  
   1.194 @@ -298,36 +340,6 @@
   1.195  
   1.196  subsection {* Strict product is a bifinite domain *}
   1.197  
   1.198 -definition
   1.199 -  sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
   1.200 -where
   1.201 -  "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   1.202 -
   1.203 -lemma sprod_approx: "approx_chain sprod_approx"
   1.204 -proof (rule approx_chain.intro)
   1.205 -  show "chain (\<lambda>i. sprod_approx i)"
   1.206 -    unfolding sprod_approx_def by simp
   1.207 -  show "(\<Squnion>i. sprod_approx i) = ID"
   1.208 -    unfolding sprod_approx_def
   1.209 -    by (simp add: lub_distribs sprod_map_ID)
   1.210 -  show "\<And>i. finite_deflation (sprod_approx i)"
   1.211 -    unfolding sprod_approx_def
   1.212 -    by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
   1.213 -qed
   1.214 -
   1.215 -definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   1.216 -where "sprod_defl = defl_fun2 sprod_approx sprod_map"
   1.217 -
   1.218 -lemma cast_sprod_defl:
   1.219 -  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
   1.220 -    udom_emb sprod_approx oo
   1.221 -      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
   1.222 -        udom_prj sprod_approx"
   1.223 -unfolding sprod_defl_def
   1.224 -apply (rule cast_defl_fun2 [OF sprod_approx])
   1.225 -apply (erule (1) finite_deflation_sprod_map)
   1.226 -done
   1.227 -
   1.228  instantiation sprod :: (bifinite, bifinite) bifinite
   1.229  begin
   1.230  
   1.231 @@ -359,32 +371,6 @@
   1.232  
   1.233  subsection {* Lifted cpo is a bifinite domain *}
   1.234  
   1.235 -definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
   1.236 -where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
   1.237 -
   1.238 -lemma u_approx: "approx_chain u_approx"
   1.239 -proof (rule approx_chain.intro)
   1.240 -  show "chain (\<lambda>i. u_approx i)"
   1.241 -    unfolding u_approx_def by simp
   1.242 -  show "(\<Squnion>i. u_approx i) = ID"
   1.243 -    unfolding u_approx_def
   1.244 -    by (simp add: lub_distribs u_map_ID)
   1.245 -  show "\<And>i. finite_deflation (u_approx i)"
   1.246 -    unfolding u_approx_def
   1.247 -    by (intro finite_deflation_u_map finite_deflation_udom_approx)
   1.248 -qed
   1.249 -
   1.250 -definition u_defl :: "defl \<rightarrow> defl"
   1.251 -where "u_defl = defl_fun1 u_approx u_map"
   1.252 -
   1.253 -lemma cast_u_defl:
   1.254 -  "cast\<cdot>(u_defl\<cdot>A) =
   1.255 -    udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
   1.256 -unfolding u_defl_def
   1.257 -apply (rule cast_defl_fun1 [OF u_approx])
   1.258 -apply (erule finite_deflation_u_map)
   1.259 -done
   1.260 -
   1.261  instantiation u :: (bifinite) bifinite
   1.262  begin
   1.263  
   1.264 @@ -500,34 +486,6 @@
   1.265  
   1.266  subsection {* Strict sum is a bifinite domain *}
   1.267  
   1.268 -definition
   1.269 -  ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
   1.270 -where
   1.271 -  "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   1.272 -
   1.273 -lemma ssum_approx: "approx_chain ssum_approx"
   1.274 -proof (rule approx_chain.intro)
   1.275 -  show "chain (\<lambda>i. ssum_approx i)"
   1.276 -    unfolding ssum_approx_def by simp
   1.277 -  show "(\<Squnion>i. ssum_approx i) = ID"
   1.278 -    unfolding ssum_approx_def
   1.279 -    by (simp add: lub_distribs ssum_map_ID)
   1.280 -  show "\<And>i. finite_deflation (ssum_approx i)"
   1.281 -    unfolding ssum_approx_def
   1.282 -    by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
   1.283 -qed
   1.284 -
   1.285 -definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl"
   1.286 -where "ssum_defl = defl_fun2 ssum_approx ssum_map"
   1.287 -
   1.288 -lemma cast_ssum_defl:
   1.289 -  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
   1.290 -    udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
   1.291 -unfolding ssum_defl_def
   1.292 -apply (rule cast_defl_fun2 [OF ssum_approx])
   1.293 -apply (erule (1) finite_deflation_ssum_map)
   1.294 -done
   1.295 -
   1.296  instantiation ssum :: (bifinite, bifinite) bifinite
   1.297  begin
   1.298  

     2.1 --- a/src/HOLCF/ConvexPD.thy	Mon Nov 08 05:07:18 2010 -0800
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Mon Nov 08 06:58:09 2010 -0800
     2.3 @@ -448,16 +448,8 @@
     2.4    "convex_approx = (\<lambda>i. convex_map\<cdot>(udom_approx i))"
     2.5  
     2.6  lemma convex_approx: "approx_chain convex_approx"
     2.7 -proof (rule approx_chain.intro)
     2.8 -  show "chain (\<lambda>i. convex_approx i)"
     2.9 -    unfolding convex_approx_def by simp
    2.10 -  show "(\<Squnion>i. convex_approx i) = ID"
    2.11 -    unfolding convex_approx_def
    2.12 -    by (simp add: lub_distribs convex_map_ID)
    2.13 -  show "\<And>i. finite_deflation (convex_approx i)"
    2.14 -    unfolding convex_approx_def
    2.15 -    by (intro finite_deflation_convex_map finite_deflation_udom_approx)
    2.16 -qed
    2.17 +using convex_map_ID finite_deflation_convex_map
    2.18 +unfolding convex_approx_def by (rule approx_chain_lemma1)
    2.19  
    2.20  definition convex_defl :: "defl \<rightarrow> defl"
    2.21  where "convex_defl = defl_fun1 convex_approx convex_map"
    2.22 @@ -465,10 +457,8 @@
    2.23  lemma cast_convex_defl:
    2.24    "cast\<cdot>(convex_defl\<cdot>A) =
    2.25      udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx"
    2.26 -unfolding convex_defl_def
    2.27 -apply (rule cast_defl_fun1 [OF convex_approx])
    2.28 -apply (erule finite_deflation_convex_map)
    2.29 -done
    2.30 +using convex_approx finite_deflation_convex_map
    2.31 +unfolding convex_defl_def by (rule cast_defl_fun1)
    2.32  
    2.33  instantiation convex_pd :: (bifinite) bifinite
    2.34  begin

     3.1 --- a/src/HOLCF/LowerPD.thy	Mon Nov 08 05:07:18 2010 -0800
     3.2 +++ b/src/HOLCF/LowerPD.thy	Mon Nov 08 06:58:09 2010 -0800
     3.3 @@ -441,16 +441,8 @@
     3.4    "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))"
     3.5  
     3.6  lemma lower_approx: "approx_chain lower_approx"
     3.7 -proof (rule approx_chain.intro)
     3.8 -  show "chain (\<lambda>i. lower_approx i)"
     3.9 -    unfolding lower_approx_def by simp
    3.10 -  show "(\<Squnion>i. lower_approx i) = ID"
    3.11 -    unfolding lower_approx_def
    3.12 -    by (simp add: lub_distribs lower_map_ID)
    3.13 -  show "\<And>i. finite_deflation (lower_approx i)"
    3.14 -    unfolding lower_approx_def
    3.15 -    by (intro finite_deflation_lower_map finite_deflation_udom_approx)
    3.16 -qed
    3.17 +using lower_map_ID finite_deflation_lower_map
    3.18 +unfolding lower_approx_def by (rule approx_chain_lemma1)
    3.19  
    3.20  definition lower_defl :: "defl \<rightarrow> defl"
    3.21  where "lower_defl = defl_fun1 lower_approx lower_map"
    3.22 @@ -458,10 +450,8 @@
    3.23  lemma cast_lower_defl:
    3.24    "cast\<cdot>(lower_defl\<cdot>A) =
    3.25      udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx"
    3.26 -unfolding lower_defl_def
    3.27 -apply (rule cast_defl_fun1 [OF lower_approx])
    3.28 -apply (erule finite_deflation_lower_map)
    3.29 -done
    3.30 +using lower_approx finite_deflation_lower_map
    3.31 +unfolding lower_defl_def by (rule cast_defl_fun1)
    3.32  
    3.33  instantiation lower_pd :: (bifinite) bifinite
    3.34  begin

     4.1 --- a/src/HOLCF/UpperPD.thy	Mon Nov 08 05:07:18 2010 -0800
     4.2 +++ b/src/HOLCF/UpperPD.thy	Mon Nov 08 06:58:09 2010 -0800
     4.3 @@ -436,16 +436,8 @@
     4.4    "upper_approx = (\<lambda>i. upper_map\<cdot>(udom_approx i))"
     4.5  
     4.6  lemma upper_approx: "approx_chain upper_approx"
     4.7 -proof (rule approx_chain.intro)
     4.8 -  show "chain (\<lambda>i. upper_approx i)"
     4.9 -    unfolding upper_approx_def by simp
    4.10 -  show "(\<Squnion>i. upper_approx i) = ID"
    4.11 -    unfolding upper_approx_def
    4.12 -    by (simp add: lub_distribs upper_map_ID)
    4.13 -  show "\<And>i. finite_deflation (upper_approx i)"
    4.14 -    unfolding upper_approx_def
    4.15 -    by (intro finite_deflation_upper_map finite_deflation_udom_approx)
    4.16 -qed
    4.17 +using upper_map_ID finite_deflation_upper_map
    4.18 +unfolding upper_approx_def by (rule approx_chain_lemma1)
    4.19  
    4.20  definition upper_defl :: "defl \<rightarrow> defl"
    4.21  where "upper_defl = defl_fun1 upper_approx upper_map"
    4.22 @@ -453,10 +445,8 @@
    4.23  lemma cast_upper_defl:
    4.24    "cast\<cdot>(upper_defl\<cdot>A) =
    4.25      udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
    4.26 -unfolding upper_defl_def
    4.27 -apply (rule cast_defl_fun1 [OF upper_approx])
    4.28 -apply (erule finite_deflation_upper_map)
    4.29 -done
    4.30 +using upper_approx finite_deflation_upper_map
    4.31 +unfolding upper_defl_def by (rule cast_defl_fun1)
    4.32  
    4.33  instantiation upper_pd :: (bifinite) bifinite
    4.34  begin