move stuff from Algebraic.thy to Bifinite.thy and elsewhere
authorhuffman
Thu Oct 07 13:54:43 2010 -0700 (2010-10-07)
changeset 39985310f98585107
parent 39984 0300d5170622
child 39986 38677db30cad
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
src/HOLCF/Algebraic.thy
src/HOLCF/Bifinite.thy
src/HOLCF/Cfun.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Cprod.thy
src/HOLCF/Deflation.thy
src/HOLCF/Sprod.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Algebraic.thy	Thu Oct 07 13:33:06 2010 -0700
     1.2 +++ b/src/HOLCF/Algebraic.thy	Thu Oct 07 13:54:43 2010 -0700
     1.3 @@ -2,10 +2,10 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -header {* Algebraic deflations and SFP domains *}
     1.8 +header {* Algebraic deflations *}
     1.9  
    1.10  theory Algebraic
    1.11 -imports Universal Bifinite
    1.12 +imports Universal
    1.13  begin
    1.14  
    1.15  subsection {* Type constructor for finite deflations *}
    1.16 @@ -257,232 +257,4 @@
    1.17  apply (simp add: in_sfp_def)
    1.18  done
    1.19  
    1.20 -subsection {* Class of SFP domains *}
    1.21 -
    1.22 -text {*
    1.23 -  We define a SFP domain as a pcpo that is isomorphic to some
    1.24 -  algebraic deflation over the universal domain.
    1.25 -*}
    1.26 -
    1.27 -class sfp = pcpo +
    1.28 -  fixes emb :: "'a::pcpo \<rightarrow> udom"
    1.29 -  fixes prj :: "udom \<rightarrow> 'a::pcpo"
    1.30 -  fixes sfp :: "'a itself \<Rightarrow> sfp"
    1.31 -  assumes ep_pair_emb_prj: "ep_pair emb prj"
    1.32 -  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
    1.33 -
    1.34 -syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
    1.35 -translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
    1.36 -
    1.37 -interpretation sfp:
    1.38 -  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
    1.39 -  unfolding pcpo_ep_pair_def
    1.40 -  by (rule ep_pair_emb_prj)
    1.41 -
    1.42 -lemmas emb_inverse = sfp.e_inverse
    1.43 -lemmas emb_prj_below = sfp.e_p_below
    1.44 -lemmas emb_eq_iff = sfp.e_eq_iff
    1.45 -lemmas emb_strict = sfp.e_strict
    1.46 -lemmas prj_strict = sfp.p_strict
    1.47 -
    1.48 -subsection {* SFP domains have a countable compact basis *}
    1.49 -
    1.50 -text {*
    1.51 -  Eventually it should be possible to generalize this to an unpointed
    1.52 -  variant of the sfp class.
    1.53 -*}
    1.54 -
    1.55 -interpretation compact_basis:
    1.56 -  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
    1.57 -proof -
    1.58 -  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
    1.59 -  and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
    1.60 -    by (rule sfp.obtain_principal_chain)
    1.61 -  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
    1.62 -  interpret sfp_approx: approx_chain approx
    1.63 -  proof (rule approx_chain.intro)
    1.64 -    show "chain (\<lambda>i. approx i)"
    1.65 -      unfolding approx_def by (simp add: Y)
    1.66 -    show "(\<Squnion>i. approx i) = ID"
    1.67 -      unfolding approx_def
    1.68 -      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
    1.69 -    show "\<And>i. finite_deflation (approx i)"
    1.70 -      unfolding approx_def
    1.71 -      apply (rule sfp.finite_deflation_p_d_e)
    1.72 -      apply (rule finite_deflation_cast)
    1.73 -      apply (rule sfp.compact_principal)
    1.74 -      apply (rule below_trans [OF monofun_cfun_fun])
    1.75 -      apply (rule is_ub_thelub, simp add: Y)
    1.76 -      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
    1.77 -      done
    1.78 -  qed
    1.79 -  (* FIXME: why does show ?thesis fail here? *)
    1.80 -  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
    1.81 -qed
    1.82 -
    1.83 -subsection {* Type combinators *}
    1.84 -
    1.85 -definition
    1.86 -  sfp_fun1 ::
    1.87 -    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
    1.88 -where
    1.89 -  "sfp_fun1 approx f =
    1.90 -    sfp.basis_fun (\<lambda>a.
    1.91 -      sfp_principal (Abs_fin_defl
    1.92 -        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
    1.93 -
    1.94 -definition
    1.95 -  sfp_fun2 ::
    1.96 -    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
    1.97 -      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
    1.98 -where
    1.99 -  "sfp_fun2 approx f =
   1.100 -    sfp.basis_fun (\<lambda>a.
   1.101 -      sfp.basis_fun (\<lambda>b.
   1.102 -        sfp_principal (Abs_fin_defl
   1.103 -          (udom_emb approx oo
   1.104 -            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
   1.105 -
   1.106 -lemma cast_sfp_fun1:
   1.107 -  assumes approx: "approx_chain approx"
   1.108 -  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
   1.109 -  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
   1.110 -proof -
   1.111 -  have 1: "\<And>a. finite_deflation
   1.112 -        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
   1.113 -    apply (rule ep_pair.finite_deflation_e_d_p)
   1.114 -    apply (rule approx_chain.ep_pair_udom [OF approx])
   1.115 -    apply (rule f, rule finite_deflation_Rep_fin_defl)
   1.116 -    done
   1.117 -  show ?thesis
   1.118 -    by (induct A rule: sfp.principal_induct, simp)
   1.119 -       (simp only: sfp_fun1_def
   1.120 -                   sfp.basis_fun_principal
   1.121 -                   sfp.basis_fun_mono
   1.122 -                   sfp.principal_mono
   1.123 -                   Abs_fin_defl_mono [OF 1 1]
   1.124 -                   monofun_cfun below_refl
   1.125 -                   Rep_fin_defl_mono
   1.126 -                   cast_sfp_principal
   1.127 -                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   1.128 -qed
   1.129 -
   1.130 -lemma cast_sfp_fun2:
   1.131 -  assumes approx: "approx_chain approx"
   1.132 -  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
   1.133 -                finite_deflation (f\<cdot>a\<cdot>b)"
   1.134 -  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
   1.135 -    udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
   1.136 -proof -
   1.137 -  have 1: "\<And>a b. finite_deflation (udom_emb approx oo
   1.138 -      f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
   1.139 -    apply (rule ep_pair.finite_deflation_e_d_p)
   1.140 -    apply (rule ep_pair_udom [OF approx])
   1.141 -    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
   1.142 -    done
   1.143 -  show ?thesis
   1.144 -    by (induct A B rule: sfp.principal_induct2, simp, simp)
   1.145 -       (simp only: sfp_fun2_def
   1.146 -                   sfp.basis_fun_principal
   1.147 -                   sfp.basis_fun_mono
   1.148 -                   sfp.principal_mono
   1.149 -                   Abs_fin_defl_mono [OF 1 1]
   1.150 -                   monofun_cfun below_refl
   1.151 -                   Rep_fin_defl_mono
   1.152 -                   cast_sfp_principal
   1.153 -                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   1.154 -qed
   1.155 -
   1.156 -subsection {* Instance for universal domain type *}
   1.157 -
   1.158 -instantiation udom :: sfp
   1.159 -begin
   1.160 -
   1.161 -definition [simp]:
   1.162 -  "emb = (ID :: udom \<rightarrow> udom)"
   1.163 -
   1.164 -definition [simp]:
   1.165 -  "prj = (ID :: udom \<rightarrow> udom)"
   1.166 -
   1.167 -definition
   1.168 -  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
   1.169 -
   1.170 -instance proof
   1.171 -  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
   1.172 -    by (simp add: ep_pair.intro)
   1.173 -next
   1.174 -  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
   1.175 -    unfolding sfp_udom_def
   1.176 -    apply (subst contlub_cfun_arg)
   1.177 -    apply (rule chainI)
   1.178 -    apply (rule sfp.principal_mono)
   1.179 -    apply (simp add: below_fin_defl_def)
   1.180 -    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
   1.181 -    apply (rule chainE)
   1.182 -    apply (rule chain_udom_approx)
   1.183 -    apply (subst cast_sfp_principal)
   1.184 -    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
   1.185 -    done
   1.186 -qed
   1.187 -
   1.188  end
   1.189 -
   1.190 -subsection {* Instance for continuous function space *}
   1.191 -
   1.192 -definition
   1.193 -  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
   1.194 -where
   1.195 -  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   1.196 -
   1.197 -lemma cfun_approx: "approx_chain cfun_approx"
   1.198 -proof (rule approx_chain.intro)
   1.199 -  show "chain (\<lambda>i. cfun_approx i)"
   1.200 -    unfolding cfun_approx_def by simp
   1.201 -  show "(\<Squnion>i. cfun_approx i) = ID"
   1.202 -    unfolding cfun_approx_def
   1.203 -    by (simp add: lub_distribs cfun_map_ID)
   1.204 -  show "\<And>i. finite_deflation (cfun_approx i)"
   1.205 -    unfolding cfun_approx_def
   1.206 -    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
   1.207 -qed
   1.208 -
   1.209 -definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   1.210 -where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
   1.211 -
   1.212 -lemma cast_cfun_sfp:
   1.213 -  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
   1.214 -    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
   1.215 -unfolding cfun_sfp_def
   1.216 -apply (rule cast_sfp_fun2 [OF cfun_approx])
   1.217 -apply (erule (1) finite_deflation_cfun_map)
   1.218 -done
   1.219 -
   1.220 -instantiation cfun :: (sfp, sfp) sfp
   1.221 -begin
   1.222 -
   1.223 -definition
   1.224 -  "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
   1.225 -
   1.226 -definition
   1.227 -  "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
   1.228 -
   1.229 -definition
   1.230 -  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   1.231 -
   1.232 -instance proof
   1.233 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   1.234 -    unfolding emb_cfun_def prj_cfun_def
   1.235 -    using ep_pair_udom [OF cfun_approx]
   1.236 -    by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
   1.237 -next
   1.238 -  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   1.239 -    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
   1.240 -    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
   1.241 -qed
   1.242 -
   1.243 -end
   1.244 -
   1.245 -lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   1.246 -by (rule sfp_cfun_def)
   1.247 -
   1.248 -end
     2.1 --- a/src/HOLCF/Bifinite.thy	Thu Oct 07 13:33:06 2010 -0700
     2.2 +++ b/src/HOLCF/Bifinite.thy	Thu Oct 07 13:54:43 2010 -0700
     2.3 @@ -2,172 +2,238 @@
     2.4      Author:     Brian Huffman
     2.5  *)
     2.6  
     2.7 -header {* Bifinite domains and approximation *}
     2.8 +header {* Bifinite domains *}
     2.9  
    2.10  theory Bifinite
    2.11 -imports Deflation
    2.12 +imports Algebraic
    2.13  begin
    2.14  
    2.15 -subsection {* Map operator for product type *}
    2.16 +subsection {* Class of SFP domains *}
    2.17 +
    2.18 +text {*
    2.19 +  We define a SFP domain as a pcpo that is isomorphic to some
    2.20 +  algebraic deflation over the universal domain.
    2.21 +*}
    2.22 +
    2.23 +class sfp = pcpo +
    2.24 +  fixes emb :: "'a::pcpo \<rightarrow> udom"
    2.25 +  fixes prj :: "udom \<rightarrow> 'a::pcpo"
    2.26 +  fixes sfp :: "'a itself \<Rightarrow> sfp"
    2.27 +  assumes ep_pair_emb_prj: "ep_pair emb prj"
    2.28 +  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
    2.29  
    2.30 -definition
    2.31 -  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    2.32 -where
    2.33 -  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    2.34 +syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
    2.35 +translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
    2.36 +
    2.37 +interpretation sfp:
    2.38 +  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
    2.39 +  unfolding pcpo_ep_pair_def
    2.40 +  by (rule ep_pair_emb_prj)
    2.41  
    2.42 -lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    2.43 -unfolding cprod_map_def by simp
    2.44 +lemmas emb_inverse = sfp.e_inverse
    2.45 +lemmas emb_prj_below = sfp.e_p_below
    2.46 +lemmas emb_eq_iff = sfp.e_eq_iff
    2.47 +lemmas emb_strict = sfp.e_strict
    2.48 +lemmas prj_strict = sfp.p_strict
    2.49  
    2.50 -lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
    2.51 -unfolding expand_cfun_eq by auto
    2.52 +subsection {* SFP domains have a countable compact basis *}
    2.53  
    2.54 -lemma cprod_map_map:
    2.55 -  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    2.56 -    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    2.57 -by (induct p) simp
    2.58 +text {*
    2.59 +  Eventually it should be possible to generalize this to an unpointed
    2.60 +  variant of the sfp class.
    2.61 +*}
    2.62  
    2.63 -lemma ep_pair_cprod_map:
    2.64 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    2.65 -  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    2.66 -proof
    2.67 -  interpret e1p1: ep_pair e1 p1 by fact
    2.68 -  interpret e2p2: ep_pair e2 p2 by fact
    2.69 -  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    2.70 -    by (induct x) simp
    2.71 -  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    2.72 -    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    2.73 +interpretation compact_basis:
    2.74 +  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
    2.75 +proof -
    2.76 +  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
    2.77 +  and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
    2.78 +    by (rule sfp.obtain_principal_chain)
    2.79 +  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
    2.80 +  interpret sfp_approx: approx_chain approx
    2.81 +  proof (rule approx_chain.intro)
    2.82 +    show "chain (\<lambda>i. approx i)"
    2.83 +      unfolding approx_def by (simp add: Y)
    2.84 +    show "(\<Squnion>i. approx i) = ID"
    2.85 +      unfolding approx_def
    2.86 +      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
    2.87 +    show "\<And>i. finite_deflation (approx i)"
    2.88 +      unfolding approx_def
    2.89 +      apply (rule sfp.finite_deflation_p_d_e)
    2.90 +      apply (rule finite_deflation_cast)
    2.91 +      apply (rule sfp.compact_principal)
    2.92 +      apply (rule below_trans [OF monofun_cfun_fun])
    2.93 +      apply (rule is_ub_thelub, simp add: Y)
    2.94 +      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
    2.95 +      done
    2.96 +  qed
    2.97 +  (* FIXME: why does show ?thesis fail here? *)
    2.98 +  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
    2.99  qed
   2.100  
   2.101 -lemma deflation_cprod_map:
   2.102 -  assumes "deflation d1" and "deflation d2"
   2.103 -  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
   2.104 -proof
   2.105 -  interpret d1: deflation d1 by fact
   2.106 -  interpret d2: deflation d2 by fact
   2.107 -  fix x
   2.108 -  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
   2.109 -    by (induct x) (simp add: d1.idem d2.idem)
   2.110 -  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   2.111 -    by (induct x) (simp add: d1.below d2.below)
   2.112 -qed
   2.113 +subsection {* Type combinators *}
   2.114 +
   2.115 +definition
   2.116 +  sfp_fun1 ::
   2.117 +    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
   2.118 +where
   2.119 +  "sfp_fun1 approx f =
   2.120 +    sfp.basis_fun (\<lambda>a.
   2.121 +      sfp_principal (Abs_fin_defl
   2.122 +        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
   2.123 +
   2.124 +definition
   2.125 +  sfp_fun2 ::
   2.126 +    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
   2.127 +      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
   2.128 +where
   2.129 +  "sfp_fun2 approx f =
   2.130 +    sfp.basis_fun (\<lambda>a.
   2.131 +      sfp.basis_fun (\<lambda>b.
   2.132 +        sfp_principal (Abs_fin_defl
   2.133 +          (udom_emb approx oo
   2.134 +            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
   2.135  
   2.136 -lemma finite_deflation_cprod_map:
   2.137 -  assumes "finite_deflation d1" and "finite_deflation d2"
   2.138 -  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
   2.139 -proof (rule finite_deflation_intro)
   2.140 -  interpret d1: finite_deflation d1 by fact
   2.141 -  interpret d2: finite_deflation d2 by fact
   2.142 -  have "deflation d1" and "deflation d2" by fact+
   2.143 -  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
   2.144 -  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
   2.145 -    by clarsimp
   2.146 -  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
   2.147 -    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   2.148 +lemma cast_sfp_fun1:
   2.149 +  assumes approx: "approx_chain approx"
   2.150 +  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
   2.151 +  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
   2.152 +proof -
   2.153 +  have 1: "\<And>a. finite_deflation
   2.154 +        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
   2.155 +    apply (rule ep_pair.finite_deflation_e_d_p)
   2.156 +    apply (rule approx_chain.ep_pair_udom [OF approx])
   2.157 +    apply (rule f, rule finite_deflation_Rep_fin_defl)
   2.158 +    done
   2.159 +  show ?thesis
   2.160 +    by (induct A rule: sfp.principal_induct, simp)
   2.161 +       (simp only: sfp_fun1_def
   2.162 +                   sfp.basis_fun_principal
   2.163 +                   sfp.basis_fun_mono
   2.164 +                   sfp.principal_mono
   2.165 +                   Abs_fin_defl_mono [OF 1 1]
   2.166 +                   monofun_cfun below_refl
   2.167 +                   Rep_fin_defl_mono
   2.168 +                   cast_sfp_principal
   2.169 +                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   2.170  qed
   2.171  
   2.172 -subsection {* Map operator for continuous function space *}
   2.173 +lemma cast_sfp_fun2:
   2.174 +  assumes approx: "approx_chain approx"
   2.175 +  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
   2.176 +                finite_deflation (f\<cdot>a\<cdot>b)"
   2.177 +  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
   2.178 +    udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
   2.179 +proof -
   2.180 +  have 1: "\<And>a b. finite_deflation (udom_emb approx oo
   2.181 +      f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
   2.182 +    apply (rule ep_pair.finite_deflation_e_d_p)
   2.183 +    apply (rule ep_pair_udom [OF approx])
   2.184 +    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
   2.185 +    done
   2.186 +  show ?thesis
   2.187 +    by (induct A B rule: sfp.principal_induct2, simp, simp)
   2.188 +       (simp only: sfp_fun2_def
   2.189 +                   sfp.basis_fun_principal
   2.190 +                   sfp.basis_fun_mono
   2.191 +                   sfp.principal_mono
   2.192 +                   Abs_fin_defl_mono [OF 1 1]
   2.193 +                   monofun_cfun below_refl
   2.194 +                   Rep_fin_defl_mono
   2.195 +                   cast_sfp_principal
   2.196 +                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
   2.197 +qed
   2.198 +
   2.199 +subsection {* Instance for universal domain type *}
   2.200 +
   2.201 +instantiation udom :: sfp
   2.202 +begin
   2.203 +
   2.204 +definition [simp]:
   2.205 +  "emb = (ID :: udom \<rightarrow> udom)"
   2.206 +
   2.207 +definition [simp]:
   2.208 +  "prj = (ID :: udom \<rightarrow> udom)"
   2.209  
   2.210  definition
   2.211 -  cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
   2.212 -where
   2.213 -  "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
   2.214 -
   2.215 -lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
   2.216 -unfolding cfun_map_def by simp
   2.217 -
   2.218 -lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
   2.219 -unfolding expand_cfun_eq by simp
   2.220 +  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
   2.221  
   2.222 -lemma cfun_map_map:
   2.223 -  "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
   2.224 -    cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   2.225 -by (rule ext_cfun) simp
   2.226 -
   2.227 -lemma ep_pair_cfun_map:
   2.228 -  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   2.229 -  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
   2.230 -proof
   2.231 -  interpret e1p1: ep_pair e1 p1 by fact
   2.232 -  interpret e2p2: ep_pair e2 p2 by fact
   2.233 -  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
   2.234 -    by (simp add: expand_cfun_eq)
   2.235 -  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
   2.236 -    apply (rule below_cfun_ext, simp)
   2.237 -    apply (rule below_trans [OF e2p2.e_p_below])
   2.238 -    apply (rule monofun_cfun_arg)
   2.239 -    apply (rule e1p1.e_p_below)
   2.240 +instance proof
   2.241 +  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
   2.242 +    by (simp add: ep_pair.intro)
   2.243 +next
   2.244 +  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
   2.245 +    unfolding sfp_udom_def
   2.246 +    apply (subst contlub_cfun_arg)
   2.247 +    apply (rule chainI)
   2.248 +    apply (rule sfp.principal_mono)
   2.249 +    apply (simp add: below_fin_defl_def)
   2.250 +    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
   2.251 +    apply (rule chainE)
   2.252 +    apply (rule chain_udom_approx)
   2.253 +    apply (subst cast_sfp_principal)
   2.254 +    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
   2.255      done
   2.256  qed
   2.257  
   2.258 -lemma deflation_cfun_map:
   2.259 -  assumes "deflation d1" and "deflation d2"
   2.260 -  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
   2.261 -proof
   2.262 -  interpret d1: deflation d1 by fact
   2.263 -  interpret d2: deflation d2 by fact
   2.264 -  fix f
   2.265 -  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
   2.266 -    by (simp add: expand_cfun_eq d1.idem d2.idem)
   2.267 -  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
   2.268 -    apply (rule below_cfun_ext, simp)
   2.269 -    apply (rule below_trans [OF d2.below])
   2.270 -    apply (rule monofun_cfun_arg)
   2.271 -    apply (rule d1.below)
   2.272 -    done
   2.273 +end
   2.274 +
   2.275 +subsection {* Instance for continuous function space *}
   2.276 +
   2.277 +definition
   2.278 +  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
   2.279 +where
   2.280 +  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
   2.281 +
   2.282 +lemma cfun_approx: "approx_chain cfun_approx"
   2.283 +proof (rule approx_chain.intro)
   2.284 +  show "chain (\<lambda>i. cfun_approx i)"
   2.285 +    unfolding cfun_approx_def by simp
   2.286 +  show "(\<Squnion>i. cfun_approx i) = ID"
   2.287 +    unfolding cfun_approx_def
   2.288 +    by (simp add: lub_distribs cfun_map_ID)
   2.289 +  show "\<And>i. finite_deflation (cfun_approx i)"
   2.290 +    unfolding cfun_approx_def
   2.291 +    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
   2.292  qed
   2.293  
   2.294 -lemma finite_range_cfun_map:
   2.295 -  assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   2.296 -  assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
   2.297 -  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
   2.298 -proof (rule finite_imageD)
   2.299 -  let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   2.300 -  show "finite (?f ` range ?h)"
   2.301 -  proof (rule finite_subset)
   2.302 -    let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
   2.303 -    show "?f ` range ?h \<subseteq> ?B"
   2.304 -      by clarsimp
   2.305 -    show "finite ?B"
   2.306 -      by (simp add: a b)
   2.307 -  qed
   2.308 -  show "inj_on ?f (range ?h)"
   2.309 -  proof (rule inj_onI, rule ext_cfun, clarsimp)
   2.310 -    fix x f g
   2.311 -    assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   2.312 -    hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   2.313 -      by (rule equalityD1)
   2.314 -    hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   2.315 -      by (simp add: subset_eq)
   2.316 -    then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
   2.317 -      by (rule rangeE)
   2.318 -    thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
   2.319 -      by clarsimp
   2.320 -  qed
   2.321 +definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
   2.322 +where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
   2.323 +
   2.324 +lemma cast_cfun_sfp:
   2.325 +  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
   2.326 +    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
   2.327 +unfolding cfun_sfp_def
   2.328 +apply (rule cast_sfp_fun2 [OF cfun_approx])
   2.329 +apply (erule (1) finite_deflation_cfun_map)
   2.330 +done
   2.331 +
   2.332 +instantiation cfun :: (sfp, sfp) sfp
   2.333 +begin
   2.334 +
   2.335 +definition
   2.336 +  "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
   2.337 +
   2.338 +definition
   2.339 +  "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
   2.340 +
   2.341 +definition
   2.342 +  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.343 +
   2.344 +instance proof
   2.345 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   2.346 +    unfolding emb_cfun_def prj_cfun_def
   2.347 +    using ep_pair_udom [OF cfun_approx]
   2.348 +    by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
   2.349 +next
   2.350 +  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
   2.351 +    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
   2.352 +    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
   2.353  qed
   2.354  
   2.355 -lemma finite_deflation_cfun_map:
   2.356 -  assumes "finite_deflation d1" and "finite_deflation d2"
   2.357 -  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   2.358 -proof (rule finite_deflation_intro)
   2.359 -  interpret d1: finite_deflation d1 by fact
   2.360 -  interpret d2: finite_deflation d2 by fact
   2.361 -  have "deflation d1" and "deflation d2" by fact+
   2.362 -  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
   2.363 -  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
   2.364 -    using d1.finite_range d2.finite_range
   2.365 -    by (rule finite_range_cfun_map)
   2.366 -  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   2.367 -    by (rule finite_range_imp_finite_fixes)
   2.368 -qed
   2.369 +end
   2.370  
   2.371 -text {* Finite deflations are compact elements of the function space *}
   2.372 -
   2.373 -lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
   2.374 -apply (frule finite_deflation_imp_deflation)
   2.375 -apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
   2.376 -apply (simp add: cfun_map_def deflation.idem eta_cfun)
   2.377 -apply (rule finite_deflation.compact)
   2.378 -apply (simp only: finite_deflation_cfun_map)
   2.379 -done
   2.380 +lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
   2.381 +by (rule sfp_cfun_def)
   2.382  
   2.383  end
     3.1 --- a/src/HOLCF/Cfun.thy	Thu Oct 07 13:33:06 2010 -0700
     3.2 +++ b/src/HOLCF/Cfun.thy	Thu Oct 07 13:54:43 2010 -0700
     3.3 @@ -96,7 +96,6 @@
     3.4  translations
     3.5    "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
     3.6  
     3.7 -
     3.8  subsection {* Continuous function space is pointed *}
     3.9  
    3.10  lemma UU_CFun: "\<bottom> \<in> CFun"
    3.11 @@ -483,7 +482,6 @@
    3.12  apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
    3.13  done
    3.14  
    3.15 -
    3.16  subsection {* Identity and composition *}
    3.17  
    3.18  definition
    3.19 @@ -530,6 +528,23 @@
    3.20  lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
    3.21  by (rule ext_cfun, simp)
    3.22  
    3.23 +subsection {* Map operator for continuous function space *}
    3.24 +
    3.25 +definition
    3.26 +  cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
    3.27 +where
    3.28 +  "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
    3.29 +
    3.30 +lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
    3.31 +unfolding cfun_map_def by simp
    3.32 +
    3.33 +lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
    3.34 +unfolding expand_cfun_eq by simp
    3.35 +
    3.36 +lemma cfun_map_map:
    3.37 +  "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    3.38 +    cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    3.39 +by (rule ext_cfun) simp
    3.40  
    3.41  subsection {* Strictified functions *}
    3.42  
     4.1 --- a/src/HOLCF/CompactBasis.thy	Thu Oct 07 13:33:06 2010 -0700
     4.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Oct 07 13:54:43 2010 -0700
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* A compact basis for powerdomains *}
     4.5  
     4.6  theory CompactBasis
     4.7 -imports Algebraic
     4.8 +imports Bifinite
     4.9  begin
    4.10  
    4.11  default_sort sfp
     5.1 --- a/src/HOLCF/Cprod.thy	Thu Oct 07 13:33:06 2010 -0700
     5.2 +++ b/src/HOLCF/Cprod.thy	Thu Oct 07 13:54:43 2010 -0700
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* The cpo of cartesian products *}
     5.5  
     5.6  theory Cprod
     5.7 -imports Algebraic
     5.8 +imports Bifinite
     5.9  begin
    5.10  
    5.11  default_sort cpo
    5.12 @@ -40,6 +40,63 @@
    5.13  lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    5.14  by (simp add: csplit_def)
    5.15  
    5.16 +subsection {* Map operator for product type *}
    5.17 +
    5.18 +definition
    5.19 +  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    5.20 +where
    5.21 +  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    5.22 +
    5.23 +lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    5.24 +unfolding cprod_map_def by simp
    5.25 +
    5.26 +lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
    5.27 +unfolding expand_cfun_eq by auto
    5.28 +
    5.29 +lemma cprod_map_map:
    5.30 +  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    5.31 +    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    5.32 +by (induct p) simp
    5.33 +
    5.34 +lemma ep_pair_cprod_map:
    5.35 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    5.36 +  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    5.37 +proof
    5.38 +  interpret e1p1: ep_pair e1 p1 by fact
    5.39 +  interpret e2p2: ep_pair e2 p2 by fact
    5.40 +  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    5.41 +    by (induct x) simp
    5.42 +  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    5.43 +    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    5.44 +qed
    5.45 +
    5.46 +lemma deflation_cprod_map:
    5.47 +  assumes "deflation d1" and "deflation d2"
    5.48 +  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
    5.49 +proof
    5.50 +  interpret d1: deflation d1 by fact
    5.51 +  interpret d2: deflation d2 by fact
    5.52 +  fix x
    5.53 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    5.54 +    by (induct x) (simp add: d1.idem d2.idem)
    5.55 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    5.56 +    by (induct x) (simp add: d1.below d2.below)
    5.57 +qed
    5.58 +
    5.59 +lemma finite_deflation_cprod_map:
    5.60 +  assumes "finite_deflation d1" and "finite_deflation d2"
    5.61 +  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
    5.62 +proof (rule finite_deflation_intro)
    5.63 +  interpret d1: finite_deflation d1 by fact
    5.64 +  interpret d2: finite_deflation d2 by fact
    5.65 +  have "deflation d1" and "deflation d2" by fact+
    5.66 +  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
    5.67 +  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    5.68 +    by clarsimp
    5.69 +  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    5.70 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    5.71 +qed
    5.72 +
    5.73  subsection {* Cartesian product is an SFP domain *}
    5.74  
    5.75  definition
     6.1 --- a/src/HOLCF/Deflation.thy	Thu Oct 07 13:33:06 2010 -0700
     6.2 +++ b/src/HOLCF/Deflation.thy	Thu Oct 07 13:54:43 2010 -0700
     6.3 @@ -405,4 +405,93 @@
     6.4  
     6.5  end
     6.6  
     6.7 +subsection {* Map operator for continuous functions *}
     6.8 +
     6.9 +lemma ep_pair_cfun_map:
    6.10 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    6.11 +  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
    6.12 +proof
    6.13 +  interpret e1p1: ep_pair e1 p1 by fact
    6.14 +  interpret e2p2: ep_pair e2 p2 by fact
    6.15 +  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    6.16 +    by (simp add: expand_cfun_eq)
    6.17 +  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
    6.18 +    apply (rule below_cfun_ext, simp)
    6.19 +    apply (rule below_trans [OF e2p2.e_p_below])
    6.20 +    apply (rule monofun_cfun_arg)
    6.21 +    apply (rule e1p1.e_p_below)
    6.22 +    done
    6.23 +qed
    6.24 +
    6.25 +lemma deflation_cfun_map:
    6.26 +  assumes "deflation d1" and "deflation d2"
    6.27 +  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
    6.28 +proof
    6.29 +  interpret d1: deflation d1 by fact
    6.30 +  interpret d2: deflation d2 by fact
    6.31 +  fix f
    6.32 +  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
    6.33 +    by (simp add: expand_cfun_eq d1.idem d2.idem)
    6.34 +  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
    6.35 +    apply (rule below_cfun_ext, simp)
    6.36 +    apply (rule below_trans [OF d2.below])
    6.37 +    apply (rule monofun_cfun_arg)
    6.38 +    apply (rule d1.below)
    6.39 +    done
    6.40 +qed
    6.41 +
    6.42 +lemma finite_range_cfun_map:
    6.43 +  assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
    6.44 +  assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
    6.45 +  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
    6.46 +proof (rule finite_imageD)
    6.47 +  let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
    6.48 +  show "finite (?f ` range ?h)"
    6.49 +  proof (rule finite_subset)
    6.50 +    let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
    6.51 +    show "?f ` range ?h \<subseteq> ?B"
    6.52 +      by clarsimp
    6.53 +    show "finite ?B"
    6.54 +      by (simp add: a b)
    6.55 +  qed
    6.56 +  show "inj_on ?f (range ?h)"
    6.57 +  proof (rule inj_onI, rule ext_cfun, clarsimp)
    6.58 +    fix x f g
    6.59 +    assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    6.60 +    hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    6.61 +      by (rule equalityD1)
    6.62 +    hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    6.63 +      by (simp add: subset_eq)
    6.64 +    then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
    6.65 +      by (rule rangeE)
    6.66 +    thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
    6.67 +      by clarsimp
    6.68 +  qed
    6.69 +qed
    6.70 +
    6.71 +lemma finite_deflation_cfun_map:
    6.72 +  assumes "finite_deflation d1" and "finite_deflation d2"
    6.73 +  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
    6.74 +proof (rule finite_deflation_intro)
    6.75 +  interpret d1: finite_deflation d1 by fact
    6.76 +  interpret d2: finite_deflation d2 by fact
    6.77 +  have "deflation d1" and "deflation d2" by fact+
    6.78 +  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
    6.79 +  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
    6.80 +    using d1.finite_range d2.finite_range
    6.81 +    by (rule finite_range_cfun_map)
    6.82 +  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
    6.83 +    by (rule finite_range_imp_finite_fixes)
    6.84 +qed
    6.85 +
    6.86 +text {* Finite deflations are compact elements of the function space *}
    6.87 +
    6.88 +lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
    6.89 +apply (frule finite_deflation_imp_deflation)
    6.90 +apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
    6.91 +apply (simp add: cfun_map_def deflation.idem eta_cfun)
    6.92 +apply (rule finite_deflation.compact)
    6.93 +apply (simp only: finite_deflation_cfun_map)
    6.94 +done
    6.95 +
    6.96  end
     7.1 --- a/src/HOLCF/Sprod.thy	Thu Oct 07 13:33:06 2010 -0700
     7.2 +++ b/src/HOLCF/Sprod.thy	Thu Oct 07 13:54:43 2010 -0700
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* The type of strict products *}
     7.5  
     7.6  theory Sprod
     7.7 -imports Algebraic
     7.8 +imports Bifinite
     7.9  begin
    7.10  
    7.11  default_sort pcpo
     8.1 --- a/src/HOLCF/Up.thy	Thu Oct 07 13:33:06 2010 -0700
     8.2 +++ b/src/HOLCF/Up.thy	Thu Oct 07 13:54:43 2010 -0700
     8.3 @@ -5,7 +5,7 @@
     8.4  header {* The type of lifted values *}
     8.5  
     8.6  theory Up
     8.7 -imports Algebraic
     8.8 +imports Bifinite
     8.9  begin
    8.10  
    8.11  default_sort cpo