1.1 --- a/src/HOLCF/Bifinite.thy	Thu Nov 05 11:36:30 2009 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Thu Nov 05 11:47:00 2009 -0800
     1.3 @@ -106,21 +106,69 @@
     1.4  
     1.5  subsection {* Instance for product type *}
     1.6  
     1.7 +definition
     1.8 +  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
     1.9 +where
    1.10 +  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    1.11 +
    1.12 +lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    1.13 +unfolding cprod_map_def by simp
    1.14 +
    1.15 +lemma ep_pair_cprod_map:
    1.16 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.17 +  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    1.18 +proof
    1.19 +  interpret e1p1: ep_pair e1 p1 by fact
    1.20 +  interpret e2p2: ep_pair e2 p2 by fact
    1.21 +  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    1.22 +    by (induct x) simp
    1.23 +  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    1.24 +    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    1.25 +qed
    1.26 +
    1.27 +lemma deflation_cprod_map:
    1.28 +  assumes "deflation d1" and "deflation d2"
    1.29 +  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
    1.30 +proof
    1.31 +  interpret d1: deflation d1 by fact
    1.32 +  interpret d2: deflation d2 by fact
    1.33 +  fix x
    1.34 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    1.35 +    by (induct x) (simp add: d1.idem d2.idem)
    1.36 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    1.37 +    by (induct x) (simp add: d1.below d2.below)
    1.38 +qed
    1.39 +
    1.40 +lemma finite_deflation_cprod_map:
    1.41 +  assumes "finite_deflation d1" and "finite_deflation d2"
    1.42 +  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
    1.43 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
    1.44 +  interpret d1: finite_deflation d1 by fact
    1.45 +  interpret d2: finite_deflation d2 by fact
    1.46 +  have "deflation d1" and "deflation d2" by fact+
    1.47 +  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
    1.48 +  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    1.49 +    by clarsimp
    1.50 +  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    1.51 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.52 +qed
    1.53 +
    1.54  instantiation "*" :: (profinite, profinite) profinite
    1.55  begin
    1.56  
    1.57 -definition approx_prod_def:
    1.58 -  "approx = (\<lambda>n. \<Lambda> x. (approx n\<cdot>(fst x), approx n\<cdot>(snd x)))"
    1.59 +definition
    1.60 +  approx_prod_def:
    1.61 +    "approx = (\<lambda>n. cprod_map\<cdot>(approx n)\<cdot>(approx n))"
    1.62  
    1.63  instance proof
    1.64    fix i :: nat and x :: "'a \<times> 'b"
    1.65    show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
    1.66      unfolding approx_prod_def by simp
    1.67    show "(\<Squnion>i. approx i\<cdot>x) = x"
    1.68 -    unfolding approx_prod_def
    1.69 +    unfolding approx_prod_def cprod_map_def
    1.70      by (simp add: lub_distribs thelub_Pair)
    1.71    show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.72 -    unfolding approx_prod_def by simp
    1.73 +    unfolding approx_prod_def cprod_map_def by simp
    1.74    have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
    1.75          {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
    1.76      unfolding approx_prod_def by clarsimp
    1.77 @@ -146,10 +194,51 @@
    1.78  
    1.79  subsection {* Instance for continuous function space *}
    1.80  
    1.81 -lemma finite_range_cfun_lemma:
    1.82 +definition
    1.83 +  cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
    1.84 +where
    1.85 +  "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
    1.86 +
    1.87 +lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
    1.88 +unfolding cfun_map_def by simp
    1.89 +
    1.90 +lemma ep_pair_cfun_map:
    1.91 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.92 +  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
    1.93 +proof
    1.94 +  interpret e1p1: ep_pair e1 p1 by fact
    1.95 +  interpret e2p2: ep_pair e2 p2 by fact
    1.96 +  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    1.97 +    by (simp add: expand_cfun_eq)
    1.98 +  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
    1.99 +    apply (rule below_cfun_ext, simp)
   1.100 +    apply (rule below_trans [OF e2p2.e_p_below])
   1.101 +    apply (rule monofun_cfun_arg)
   1.102 +    apply (rule e1p1.e_p_below)
   1.103 +    done
   1.104 +qed
   1.105 +
   1.106 +lemma deflation_cfun_map:
   1.107 +  assumes "deflation d1" and "deflation d2"
   1.108 +  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
   1.109 +proof
   1.110 +  interpret d1: deflation d1 by fact
   1.111 +  interpret d2: deflation d2 by fact
   1.112 +  fix f
   1.113 +  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
   1.114 +    by (simp add: expand_cfun_eq d1.idem d2.idem)
   1.115 +  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
   1.116 +    apply (rule below_cfun_ext, simp)
   1.117 +    apply (rule below_trans [OF d2.below])
   1.118 +    apply (rule monofun_cfun_arg)
   1.119 +    apply (rule d1.below)
   1.120 +    done
   1.121 +qed
   1.122 +
   1.123 +lemma finite_range_cfun_map:
   1.124    assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   1.125    assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
   1.126 -  shows "finite (range (\<lambda>f. \<Lambda> x. b\<cdot>(f\<cdot>(a\<cdot>x))))"  (is "finite (range ?h)")
   1.127 +  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
   1.128  proof (rule finite_imageD)
   1.129    let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   1.130    show "finite (?f ` range ?h)"
   1.131 @@ -175,12 +264,27 @@
   1.132    qed
   1.133  qed
   1.134  
   1.135 +lemma finite_deflation_cfun_map:
   1.136 +  assumes "finite_deflation d1" and "finite_deflation d2"
   1.137 +  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   1.138 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
   1.139 +  interpret d1: finite_deflation d1 by fact
   1.140 +  interpret d2: finite_deflation d2 by fact
   1.141 +  have "deflation d1" and "deflation d2" by fact+
   1.142 +  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
   1.143 +  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
   1.144 +    using d1.finite_range d2.finite_range
   1.145 +    by (rule finite_range_cfun_map)
   1.146 +  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   1.147 +    by (rule finite_range_imp_finite_fixes)
   1.148 +qed
   1.149 +
   1.150  instantiation "->" :: (profinite, profinite) profinite
   1.151  begin
   1.152  
   1.153  definition
   1.154    approx_cfun_def:
   1.155 -    "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
   1.156 +    "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"
   1.157  
   1.158  instance proof
   1.159    show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))"
   1.160 @@ -188,19 +292,19 @@
   1.161  next
   1.162    fix x :: "'a \<rightarrow> 'b"
   1.163    show "(\<Squnion>i. approx i\<cdot>x) = x"
   1.164 -    unfolding approx_cfun_def
   1.165 +    unfolding approx_cfun_def cfun_map_def
   1.166      by (simp add: lub_distribs eta_cfun)
   1.167  next
   1.168    fix i :: nat and x :: "'a \<rightarrow> 'b"
   1.169    show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   1.170 -    unfolding approx_cfun_def by simp
   1.171 +    unfolding approx_cfun_def cfun_map_def by simp
   1.172  next
   1.173    fix i :: nat
   1.174    show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}"
   1.175 -    apply (rule finite_range_imp_finite_fixes)
   1.176 -    apply (simp add: approx_cfun_def)
   1.177 -    apply (intro finite_range_cfun_lemma finite_range_approx)
   1.178 -    done
   1.179 +    unfolding approx_cfun_def
   1.180 +    by (intro finite_deflation.finite_fixes
   1.181 +              finite_deflation_cfun_map
   1.182 +              finite_deflation_approx)
   1.183  qed
   1.184  
   1.185  end

     2.1 --- a/src/HOLCF/Domain.thy	Thu Nov 05 11:36:30 2009 -0800
     2.2 +++ b/src/HOLCF/Domain.thy	Thu Nov 05 11:47:00 2009 -0800
     2.3 @@ -204,61 +204,11 @@
     2.4  
     2.5  subsection {* Combinators for building copy functions *}
     2.6  
     2.7 -definition
     2.8 -  cfun_fun :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
     2.9 -where
    2.10 -  "cfun_fun = (\<Lambda> f g p. g oo p oo f)"
    2.11 +lemmas domain_map_stricts =
    2.12 +  ssum_map_strict sprod_map_strict u_map_strict
    2.13  
    2.14 -definition
    2.15 -  ssum_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
    2.16 -where
    2.17 -  "ssum_fun = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
    2.18 -
    2.19 -definition
    2.20 -  sprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
    2.21 -where
    2.22 -  "sprod_fun = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
    2.23 -
    2.24 -definition
    2.25 -  cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    2.26 -where
    2.27 -  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. (f\<cdot>x, g\<cdot>y)))"
    2.28 -
    2.29 -definition
    2.30 -  u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
    2.31 -where
    2.32 -  "u_fun = (\<Lambda> f. fup\<cdot>(up oo f))"
    2.33 -
    2.34 -lemma cfun_fun_strict: "b\<cdot>\<bottom> = \<bottom> \<Longrightarrow> cfun_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
    2.35 -unfolding cfun_fun_def expand_cfun_eq by simp
    2.36 -
    2.37 -lemma ssum_fun_strict: "ssum_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
    2.38 -unfolding ssum_fun_def by simp
    2.39 -
    2.40 -lemma sprod_fun_strict: "sprod_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
    2.41 -unfolding sprod_fun_def by simp
    2.42 -
    2.43 -lemma u_fun_strict: "u_fun\<cdot>a\<cdot>\<bottom> = \<bottom>"
    2.44 -unfolding u_fun_def by simp
    2.45 -
    2.46 -lemma ssum_fun_sinl: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
    2.47 -by (simp add: ssum_fun_def)
    2.48 -
    2.49 -lemma ssum_fun_sinr: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
    2.50 -by (simp add: ssum_fun_def)
    2.51 -
    2.52 -lemma sprod_fun_spair:
    2.53 -  "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_fun\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
    2.54 -by (simp add: sprod_fun_def)
    2.55 -
    2.56 -lemma u_fun_up: "u_fun\<cdot>a\<cdot>(up\<cdot>x) = up\<cdot>(a\<cdot>x)"
    2.57 -by (simp add: u_fun_def)
    2.58 -
    2.59 -lemmas domain_fun_stricts =
    2.60 -  ssum_fun_strict sprod_fun_strict u_fun_strict
    2.61 -
    2.62 -lemmas domain_fun_simps =
    2.63 -  ssum_fun_sinl ssum_fun_sinr sprod_fun_spair u_fun_up
    2.64 +lemmas domain_map_simps =
    2.65 +  ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
    2.66  
    2.67  
    2.68  subsection {* Installing the domain package *}

     3.1 --- a/src/HOLCF/Sprod.thy	Thu Nov 05 11:36:30 2009 -0800
     3.2 +++ b/src/HOLCF/Sprod.thy	Thu Nov 05 11:47:00 2009 -0800
     3.3 @@ -131,6 +131,9 @@
     3.4  lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
     3.5  by simp
     3.6  
     3.7 +lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
     3.8 +by (cases p, simp only: inst_sprod_pcpo2, simp)
     3.9 +
    3.10  subsection {* Properties of @{term sfst} and @{term ssnd} *}
    3.11  
    3.12  lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
    3.13 @@ -228,6 +231,68 @@
    3.14      done
    3.15  qed
    3.16  
    3.17 +subsection {* Map function for strict products *}
    3.18 +
    3.19 +definition
    3.20 +  sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
    3.21 +where
    3.22 +  "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
    3.23 +
    3.24 +lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
    3.25 +unfolding sprod_map_def by simp
    3.26 +
    3.27 +lemma sprod_map_spair [simp]:
    3.28 +  "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
    3.29 +by (simp add: sprod_map_def)
    3.30 +
    3.31 +lemma ep_pair_sprod_map:
    3.32 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    3.33 +  shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
    3.34 +proof
    3.35 +  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
    3.36 +  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
    3.37 +  fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    3.38 +    by (induct x) simp_all
    3.39 +  fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    3.40 +    apply (induct y, simp)
    3.41 +    apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
    3.42 +    apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
    3.43 +    done
    3.44 +qed
    3.45 +
    3.46 +lemma deflation_sprod_map:
    3.47 +  assumes "deflation d1" and "deflation d2"
    3.48 +  shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
    3.49 +proof
    3.50 +  interpret d1: deflation d1 by fact
    3.51 +  interpret d2: deflation d2 by fact
    3.52 +  fix x
    3.53 +  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    3.54 +    apply (induct x, simp)
    3.55 +    apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
    3.56 +    apply (simp add: d1.idem d2.idem)
    3.57 +    done
    3.58 +  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    3.59 +    apply (induct x, simp)
    3.60 +    apply (simp add: monofun_cfun d1.below d2.below)
    3.61 +    done
    3.62 +qed
    3.63 +
    3.64 +lemma finite_deflation_sprod_map:
    3.65 +  assumes "finite_deflation d1" and "finite_deflation d2"
    3.66 +  shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
    3.67 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
    3.68 +  interpret d1: finite_deflation d1 by fact
    3.69 +  interpret d2: finite_deflation d2 by fact
    3.70 +  have "deflation d1" and "deflation d2" by fact+
    3.71 +  thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
    3.72 +  have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
    3.73 +        ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
    3.74 +    by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
    3.75 +  thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
    3.76 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    3.77 +qed
    3.78 +
    3.79  subsection {* Strict product is a bifinite domain *}
    3.80  
    3.81  instantiation "**" :: (bifinite, bifinite) bifinite
    3.82 @@ -235,35 +300,30 @@
    3.83  
    3.84  definition
    3.85    approx_sprod_def:
    3.86 -    "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
    3.87 +    "approx = (\<lambda>n. sprod_map\<cdot>(approx n)\<cdot>(approx n))"
    3.88  
    3.89  instance proof
    3.90    fix i :: nat and x :: "'a \<otimes> 'b"
    3.91    show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
    3.92      unfolding approx_sprod_def by simp
    3.93    show "(\<Squnion>i. approx i\<cdot>x) = x"
    3.94 -    unfolding approx_sprod_def
    3.95 +    unfolding approx_sprod_def sprod_map_def
    3.96      by (simp add: lub_distribs eta_cfun)
    3.97    show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    3.98 +    unfolding approx_sprod_def sprod_map_def
    3.99 +    by (simp add: ssplit_def strictify_conv_if)
   3.100 +  show "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
   3.101      unfolding approx_sprod_def
   3.102 -    by (simp add: ssplit_def strictify_conv_if)
   3.103 -  have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
   3.104 -    unfolding approx_sprod_def
   3.105 -    apply (clarify, case_tac x)
   3.106 -     apply (simp add: Rep_Sprod_strict)
   3.107 -    apply (simp add: Rep_Sprod_spair spair_eq_iff)
   3.108 -    done
   3.109 -  hence "finite (Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x})"
   3.110 -    using finite_fixes_approx by (rule finite_subset)
   3.111 -  thus "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
   3.112 -    by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
   3.113 +    by (intro finite_deflation.finite_fixes
   3.114 +              finite_deflation_sprod_map
   3.115 +              finite_deflation_approx)
   3.116  qed
   3.117  
   3.118  end
   3.119  
   3.120  lemma approx_spair [simp]:
   3.121    "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
   3.122 -unfolding approx_sprod_def
   3.123 +unfolding approx_sprod_def sprod_map_def
   3.124  by (simp add: ssplit_def strictify_conv_if)
   3.125  
   3.126  end

     4.1 --- a/src/HOLCF/Ssum.thy	Thu Nov 05 11:36:30 2009 -0800
     4.2 +++ b/src/HOLCF/Ssum.thy	Thu Nov 05 11:47:00 2009 -0800
     4.3 @@ -210,6 +210,72 @@
     4.4  apply (case_tac y, simp_all add: flat_below_iff)
     4.5  done
     4.6  
     4.7 +subsection {* Map function for strict sums *}
     4.8 +
     4.9 +definition
    4.10 +  ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
    4.11 +where
    4.12 +  "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
    4.13 +
    4.14 +lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
    4.15 +unfolding ssum_map_def by simp
    4.16 +
    4.17 +lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
    4.18 +unfolding ssum_map_def by simp
    4.19 +
    4.20 +lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
    4.21 +unfolding ssum_map_def by simp
    4.22 +
    4.23 +lemma ep_pair_ssum_map:
    4.24 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    4.25 +  shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
    4.26 +proof
    4.27 +  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
    4.28 +  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
    4.29 +  fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    4.30 +    by (induct x) simp_all
    4.31 +  fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    4.32 +    apply (induct y, simp)
    4.33 +    apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
    4.34 +    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
    4.35 +    done
    4.36 +qed
    4.37 +
    4.38 +lemma deflation_ssum_map:
    4.39 +  assumes "deflation d1" and "deflation d2"
    4.40 +  shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
    4.41 +proof
    4.42 +  interpret d1: deflation d1 by fact
    4.43 +  interpret d2: deflation d2 by fact
    4.44 +  fix x
    4.45 +  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
    4.46 +    apply (induct x, simp)
    4.47 +    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
    4.48 +    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
    4.49 +    done
    4.50 +  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    4.51 +    apply (induct x, simp)
    4.52 +    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
    4.53 +    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
    4.54 +    done
    4.55 +qed
    4.56 +
    4.57 +lemma finite_deflation_ssum_map:
    4.58 +  assumes "finite_deflation d1" and "finite_deflation d2"
    4.59 +  shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
    4.60 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
    4.61 +  interpret d1: finite_deflation d1 by fact
    4.62 +  interpret d2: finite_deflation d2 by fact
    4.63 +  have "deflation d1" and "deflation d2" by fact+
    4.64 +  thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
    4.65 +  have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
    4.66 +        (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
    4.67 +        (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
    4.68 +    by (rule subsetI, case_tac x, simp_all)
    4.69 +  thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
    4.70 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    4.71 +qed
    4.72 +
    4.73  subsection {* Strict sum is a bifinite domain *}
    4.74  
    4.75  instantiation "++" :: (bifinite, bifinite) bifinite
    4.76 @@ -217,7 +283,7 @@
    4.77  
    4.78  definition
    4.79    approx_ssum_def:
    4.80 -    "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
    4.81 +    "approx = (\<lambda>n. ssum_map\<cdot>(approx n)\<cdot>(approx n))"
    4.82  
    4.83  lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
    4.84  unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
    4.85 @@ -231,16 +297,14 @@
    4.86      unfolding approx_ssum_def by simp
    4.87    show "(\<Squnion>i. approx i\<cdot>x) = x"
    4.88      unfolding approx_ssum_def
    4.89 -    by (simp add: lub_distribs eta_cfun)
    4.90 +    by (cases x, simp_all add: lub_distribs)
    4.91    show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    4.92      by (cases x, simp add: approx_ssum_def, simp, simp)
    4.93 -  have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
    4.94 -        (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
    4.95 -        (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
    4.96 -    by (rule subsetI, case_tac x rule: ssumE2, simp, simp)
    4.97 -  thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
    4.98 -    by (rule finite_subset,
    4.99 -        intro finite_UnI finite_imageI finite_fixes_approx)
   4.100 +  show "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
   4.101 +    unfolding approx_ssum_def
   4.102 +    by (intro finite_deflation.finite_fixes
   4.103 +              finite_deflation_ssum_map
   4.104 +              finite_deflation_approx)
   4.105  qed
   4.106  
   4.107  end

     5.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 05 11:36:30 2009 -0800
     5.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 05 11:47:00 2009 -0800
     5.3 @@ -28,11 +28,11 @@
     5.4  
     5.5  (* FIXME: use theory data for this *)
     5.6  val copy_tab : string Symtab.table =
     5.7 -    Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
     5.8 -                 (@{type_name "++"}, @{const_name "ssum_fun"}),
     5.9 -                 (@{type_name "**"}, @{const_name "sprod_fun"}),
    5.10 -                 (@{type_name "*"}, @{const_name "cprod_fun"}),
    5.11 -                 (@{type_name "u"}, @{const_name "u_fun"})];
    5.12 +    Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
    5.13 +                 (@{type_name "++"}, @{const_name "ssum_map"}),
    5.14 +                 (@{type_name "**"}, @{const_name "sprod_map"}),
    5.15 +                 (@{type_name "*"}, @{const_name "cprod_map"}),
    5.16 +                 (@{type_name "u"}, @{const_name "u_map"})];
    5.17  
    5.18  fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
    5.19  and copy r (DatatypeAux.DtRec i) = r i

     6.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 05 11:36:30 2009 -0800
     6.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 05 11:47:00 2009 -0800
     6.3 @@ -589,7 +589,7 @@
     6.4    let
     6.5      val _ = trace " Proving copy_strict...";
     6.6      val goal = mk_trp (strict (dc_copy `% "f"));
     6.7 -    val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts};
     6.8 +    val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
     6.9      val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
    6.10    in pg [ax_copy_def] goal (K tacs) end;
    6.11  
    6.12 @@ -604,9 +604,9 @@
    6.13        val rhs = con_app2 con one_rhs args;
    6.14        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    6.15        val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
    6.16 -      val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
    6.17 +      val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
    6.18        fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
    6.19 -      val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
    6.20 +      val rules = [ax_abs_iso] @ @{thms domain_map_simps};
    6.21        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
    6.22      in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    6.23  in

     7.1 --- a/src/HOLCF/Up.thy	Thu Nov 05 11:36:30 2009 -0800
     7.2 +++ b/src/HOLCF/Up.thy	Thu Nov 05 11:47:00 2009 -0800
     7.3 @@ -290,6 +290,43 @@
     7.4  lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
     7.5  by (cases x, simp_all)
     7.6  
     7.7 +subsection {* Map function for lifted cpo *}
     7.8 +
     7.9 +definition
    7.10 +  u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
    7.11 +where
    7.12 +  "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
    7.13 +
    7.14 +lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
    7.15 +unfolding u_map_def by simp
    7.16 +
    7.17 +lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
    7.18 +unfolding u_map_def by simp
    7.19 +
    7.20 +lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
    7.21 +apply default
    7.22 +apply (case_tac x, simp, simp add: ep_pair.e_inverse)
    7.23 +apply (case_tac y, simp, simp add: ep_pair.e_p_below)
    7.24 +done
    7.25 +
    7.26 +lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
    7.27 +apply default
    7.28 +apply (case_tac x, simp, simp add: deflation.idem)
    7.29 +apply (case_tac x, simp, simp add: deflation.below)
    7.30 +done
    7.31 +
    7.32 +lemma finite_deflation_u_map:
    7.33 +  assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
    7.34 +proof (intro finite_deflation.intro finite_deflation_axioms.intro)
    7.35 +  interpret d: finite_deflation d by fact
    7.36 +  have "deflation d" by fact
    7.37 +  thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
    7.38 +  have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
    7.39 +    by (rule subsetI, case_tac x, simp_all)
    7.40 +  thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
    7.41 +    by (rule finite_subset, simp add: d.finite_fixes)
    7.42 +qed
    7.43 +
    7.44  subsection {* Lifted cpo is a bifinite domain *}
    7.45  
    7.46  instantiation u :: (profinite) bifinite
    7.47 @@ -297,7 +334,7 @@
    7.48  
    7.49  definition
    7.50    approx_up_def:
    7.51 -    "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
    7.52 +    "approx = (\<lambda>n. u_map\<cdot>(approx n))"
    7.53  
    7.54  instance proof
    7.55    fix i :: nat and x :: "'a u"
    7.56 @@ -305,16 +342,15 @@
    7.57      unfolding approx_up_def by simp
    7.58    show "(\<Squnion>i. approx i\<cdot>x) = x"
    7.59      unfolding approx_up_def
    7.60 -    by (simp add: lub_distribs eta_cfun)
    7.61 +    by (induct x, simp, simp add: lub_distribs)
    7.62    show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    7.63      unfolding approx_up_def
    7.64 -    by (induct x, simp, simp)
    7.65 -  have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
    7.66 -        insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
    7.67 +    by (induct x) simp_all
    7.68 +  show "finite {x::'a u. approx i\<cdot>x = x}"
    7.69      unfolding approx_up_def
    7.70 -    by (rule subsetI, case_tac x, simp_all)
    7.71 -  thus "finite {x::'a u. approx i\<cdot>x = x}"
    7.72 -    by (rule finite_subset, simp add: finite_fixes_approx)
    7.73 +    by (intro finite_deflation.finite_fixes
    7.74 +              finite_deflation_u_map
    7.75 +              finite_deflation_approx)
    7.76  qed
    7.77  
    7.78  end