# HG changeset patch
# User huffman
# Date 1257450420 28800
# Node ID b4210cc3ac97036ad4fcd583f85da74d8938543f
# Parent  3496616b2171685437e43ec0d901b9520ed153a4
map functions for various types, with ep_pair/deflation/finite_deflation lemmas

diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Bifinite.thy	Thu Nov 05 11:47:00 2009 -0800
@@ -106,21 +106,69 @@
 
 subsection {* Instance for product type *}
 
+definition
+  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
+where
+  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
+
+lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
+unfolding cprod_map_def by simp
+
+lemma ep_pair_cprod_map:
+  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
+proof
+  interpret e1p1: ep_pair e1 p1 by fact
+  interpret e2p2: ep_pair e2 p2 by fact
+  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+    by (induct x) simp
+  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
+qed
+
+lemma deflation_cprod_map:
+  assumes "deflation d1" and "deflation d2"
+  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof
+  interpret d1: deflation d1 by fact
+  interpret d2: deflation d2 by fact
+  fix x
+  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+    by (induct x) (simp add: d1.idem d2.idem)
+  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+    by (induct x) (simp add: d1.below d2.below)
+qed
+
+lemma finite_deflation_cprod_map:
+  assumes "finite_deflation d1" and "finite_deflation d2"
+  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d1: finite_deflation d1 by fact
+  interpret d2: finite_deflation d2 by fact
+  have "deflation d1" and "deflation d2" by fact+
+  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
+  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
+    by clarsimp
+  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
+    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
 instantiation "*" :: (profinite, profinite) profinite
 begin
 
-definition approx_prod_def:
-  "approx = (\<lambda>n. \<Lambda> x. (approx n\<cdot>(fst x), approx n\<cdot>(snd x)))"
+definition
+  approx_prod_def:
+    "approx = (\<lambda>n. cprod_map\<cdot>(approx n)\<cdot>(approx n))"
 
 instance proof
   fix i :: nat and x :: "'a \<times> 'b"
   show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
     unfolding approx_prod_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
-    unfolding approx_prod_def
+    unfolding approx_prod_def cprod_map_def
     by (simp add: lub_distribs thelub_Pair)
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
-    unfolding approx_prod_def by simp
+    unfolding approx_prod_def cprod_map_def by simp
   have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
         {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
     unfolding approx_prod_def by clarsimp
@@ -146,10 +194,51 @@
 
 subsection {* Instance for continuous function space *}
 
-lemma finite_range_cfun_lemma:
+definition
+  cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
+where
+  "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
+
+lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
+unfolding cfun_map_def by simp
+
+lemma ep_pair_cfun_map:
+  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
+proof
+  interpret e1p1: ep_pair e1 p1 by fact
+  interpret e2p2: ep_pair e2 p2 by fact
+  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+    by (simp add: expand_cfun_eq)
+  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+    apply (rule below_cfun_ext, simp)
+    apply (rule below_trans [OF e2p2.e_p_below])
+    apply (rule monofun_cfun_arg)
+    apply (rule e1p1.e_p_below)
+    done
+qed
+
+lemma deflation_cfun_map:
+  assumes "deflation d1" and "deflation d2"
+  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
+proof
+  interpret d1: deflation d1 by fact
+  interpret d2: deflation d2 by fact
+  fix f
+  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
+    by (simp add: expand_cfun_eq d1.idem d2.idem)
+  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
+    apply (rule below_cfun_ext, simp)
+    apply (rule below_trans [OF d2.below])
+    apply (rule monofun_cfun_arg)
+    apply (rule d1.below)
+    done
+qed
+
+lemma finite_range_cfun_map:
   assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
-  shows "finite (range (\<lambda>f. \<Lambda> x. b\<cdot>(f\<cdot>(a\<cdot>x))))"  (is "finite (range ?h)")
+  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
 proof (rule finite_imageD)
   let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   show "finite (?f ` range ?h)"
@@ -175,12 +264,27 @@
   qed
 qed
 
+lemma finite_deflation_cfun_map:
+  assumes "finite_deflation d1" and "finite_deflation d2"
+  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d1: finite_deflation d1 by fact
+  interpret d2: finite_deflation d2 by fact
+  have "deflation d1" and "deflation d2" by fact+
+  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
+  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
+    using d1.finite_range d2.finite_range
+    by (rule finite_range_cfun_map)
+  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+    by (rule finite_range_imp_finite_fixes)
+qed
+
 instantiation "->" :: (profinite, profinite) profinite
 begin
 
 definition
   approx_cfun_def:
-    "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
+    "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"
 
 instance proof
   show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))"
@@ -188,19 +292,19 @@
 next
   fix x :: "'a \<rightarrow> 'b"
   show "(\<Squnion>i. approx i\<cdot>x) = x"
-    unfolding approx_cfun_def
+    unfolding approx_cfun_def cfun_map_def
     by (simp add: lub_distribs eta_cfun)
 next
   fix i :: nat and x :: "'a \<rightarrow> 'b"
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
-    unfolding approx_cfun_def by simp
+    unfolding approx_cfun_def cfun_map_def by simp
 next
   fix i :: nat
   show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}"
-    apply (rule finite_range_imp_finite_fixes)
-    apply (simp add: approx_cfun_def)
-    apply (intro finite_range_cfun_lemma finite_range_approx)
-    done
+    unfolding approx_cfun_def
+    by (intro finite_deflation.finite_fixes
+              finite_deflation_cfun_map
+              finite_deflation_approx)
 qed
 
 end
diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Domain.thy	Thu Nov 05 11:47:00 2009 -0800
@@ -204,61 +204,11 @@
 
 subsection {* Combinators for building copy functions *}
 
-definition
-  cfun_fun :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
-where
-  "cfun_fun = (\<Lambda> f g p. g oo p oo f)"
-
-definition
-  ssum_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
-where
-  "ssum_fun = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
-
-definition
-  sprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
-where
-  "sprod_fun = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
-
-definition
-  cprod_fun :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
-where
-  "cprod_fun = (\<Lambda> f g. csplit\<cdot>(\<Lambda> x y. (f\<cdot>x, g\<cdot>y)))"
-
-definition
-  u_fun :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
-where
-  "u_fun = (\<Lambda> f. fup\<cdot>(up oo f))"
-
-lemma cfun_fun_strict: "b\<cdot>\<bottom> = \<bottom> \<Longrightarrow> cfun_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding cfun_fun_def expand_cfun_eq by simp
+lemmas domain_map_stricts =
+  ssum_map_strict sprod_map_strict u_map_strict
 
-lemma ssum_fun_strict: "ssum_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding ssum_fun_def by simp
-
-lemma sprod_fun_strict: "sprod_fun\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
-unfolding sprod_fun_def by simp
-
-lemma u_fun_strict: "u_fun\<cdot>a\<cdot>\<bottom> = \<bottom>"
-unfolding u_fun_def by simp
-
-lemma ssum_fun_sinl: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
-by (simp add: ssum_fun_def)
-
-lemma ssum_fun_sinr: "x \<noteq> \<bottom> \<Longrightarrow> ssum_fun\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
-by (simp add: ssum_fun_def)
-
-lemma sprod_fun_spair:
-  "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_fun\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
-by (simp add: sprod_fun_def)
-
-lemma u_fun_up: "u_fun\<cdot>a\<cdot>(up\<cdot>x) = up\<cdot>(a\<cdot>x)"
-by (simp add: u_fun_def)
-
-lemmas domain_fun_stricts =
-  ssum_fun_strict sprod_fun_strict u_fun_strict
-
-lemmas domain_fun_simps =
-  ssum_fun_sinl ssum_fun_sinr sprod_fun_spair u_fun_up
+lemmas domain_map_simps =
+  ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
 
 
 subsection {* Installing the domain package *}
diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Sprod.thy	Thu Nov 05 11:47:00 2009 -0800
@@ -131,6 +131,9 @@
 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
 by simp
 
+lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
+by (cases p, simp only: inst_sprod_pcpo2, simp)
+
 subsection {* Properties of @{term sfst} and @{term ssnd} *}
 
 lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
@@ -228,6 +231,68 @@
     done
 qed
 
+subsection {* Map function for strict products *}
+
+definition
+  sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
+where
+  "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
+
+lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
+unfolding sprod_map_def by simp
+
+lemma sprod_map_spair [simp]:
+  "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
+by (simp add: sprod_map_def)
+
+lemma ep_pair_sprod_map:
+  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+  shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
+proof
+  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
+  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
+  fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+    by (induct x) simp_all
+  fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+    apply (induct y, simp)
+    apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
+    apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
+    done
+qed
+
+lemma deflation_sprod_map:
+  assumes "deflation d1" and "deflation d2"
+  shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
+proof
+  interpret d1: deflation d1 by fact
+  interpret d2: deflation d2 by fact
+  fix x
+  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
+    apply (induct x, simp)
+    apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
+    apply (simp add: d1.idem d2.idem)
+    done
+  show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+    apply (induct x, simp)
+    apply (simp add: monofun_cfun d1.below d2.below)
+    done
+qed
+
+lemma finite_deflation_sprod_map:
+  assumes "finite_deflation d1" and "finite_deflation d2"
+  shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d1: finite_deflation d1 by fact
+  interpret d2: finite_deflation d2 by fact
+  have "deflation d1" and "deflation d2" by fact+
+  thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
+  have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
+        ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
+    by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
+  thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
 subsection {* Strict product is a bifinite domain *}
 
 instantiation "**" :: (bifinite, bifinite) bifinite
@@ -235,35 +300,30 @@
 
 definition
   approx_sprod_def:
-    "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
+    "approx = (\<lambda>n. sprod_map\<cdot>(approx n)\<cdot>(approx n))"
 
 instance proof
   fix i :: nat and x :: "'a \<otimes> 'b"
   show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
     unfolding approx_sprod_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
-    unfolding approx_sprod_def
+    unfolding approx_sprod_def sprod_map_def
     by (simp add: lub_distribs eta_cfun)
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
-    unfolding approx_sprod_def
+    unfolding approx_sprod_def sprod_map_def
     by (simp add: ssplit_def strictify_conv_if)
-  have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
+  show "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
     unfolding approx_sprod_def
-    apply (clarify, case_tac x)
-     apply (simp add: Rep_Sprod_strict)
-    apply (simp add: Rep_Sprod_spair spair_eq_iff)
-    done
-  hence "finite (Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x})"
-    using finite_fixes_approx by (rule finite_subset)
-  thus "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
-    by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
+    by (intro finite_deflation.finite_fixes
+              finite_deflation_sprod_map
+              finite_deflation_approx)
 qed
 
 end
 
 lemma approx_spair [simp]:
   "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
-unfolding approx_sprod_def
+unfolding approx_sprod_def sprod_map_def
 by (simp add: ssplit_def strictify_conv_if)
 
 end
diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Ssum.thy	Thu Nov 05 11:47:00 2009 -0800
@@ -210,6 +210,72 @@
 apply (case_tac y, simp_all add: flat_below_iff)
 done
 
+subsection {* Map function for strict sums *}
+
+definition
+  ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
+where
+  "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
+
+lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+unfolding ssum_map_def by simp
+
+lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+unfolding ssum_map_def by simp
+
+lemma ep_pair_ssum_map:
+  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
+  shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
+proof
+  interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
+  interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
+  fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
+    by (induct x) simp_all
+  fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
+    apply (induct y, simp)
+    apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
+    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
+    done
+qed
+
+lemma deflation_ssum_map:
+  assumes "deflation d1" and "deflation d2"
+  shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
+proof
+  interpret d1: deflation d1 by fact
+  interpret d2: deflation d2 by fact
+  fix x
+  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
+    apply (induct x, simp)
+    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
+    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
+    done
+  show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
+    apply (induct x, simp)
+    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
+    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
+    done
+qed
+
+lemma finite_deflation_ssum_map:
+  assumes "finite_deflation d1" and "finite_deflation d2"
+  shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d1: finite_deflation d1 by fact
+  interpret d2: finite_deflation d2 by fact
+  have "deflation d1" and "deflation d2" by fact+
+  thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
+  have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
+        (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
+        (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
+    by (rule subsetI, case_tac x, simp_all)
+  thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
+    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
+qed
+
 subsection {* Strict sum is a bifinite domain *}
 
 instantiation "++" :: (bifinite, bifinite) bifinite
@@ -217,7 +283,7 @@
 
 definition
   approx_ssum_def:
-    "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
+    "approx = (\<lambda>n. ssum_map\<cdot>(approx n)\<cdot>(approx n))"
 
 lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
@@ -231,16 +297,14 @@
     unfolding approx_ssum_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_ssum_def
-    by (simp add: lub_distribs eta_cfun)
+    by (cases x, simp_all add: lub_distribs)
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
     by (cases x, simp add: approx_ssum_def, simp, simp)
-  have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
-        (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
-        (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
-    by (rule subsetI, case_tac x rule: ssumE2, simp, simp)
-  thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
-    by (rule finite_subset,
-        intro finite_UnI finite_imageI finite_fixes_approx)
+  show "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
+    unfolding approx_ssum_def
+    by (intro finite_deflation.finite_fixes
+              finite_deflation_ssum_map
+              finite_deflation_approx)
 qed
 
 end
diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 05 11:47:00 2009 -0800
@@ -28,11 +28,11 @@
 
 (* FIXME: use theory data for this *)
 val copy_tab : string Symtab.table =
-    Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
-                 (@{type_name "++"}, @{const_name "ssum_fun"}),
-                 (@{type_name "**"}, @{const_name "sprod_fun"}),
-                 (@{type_name "*"}, @{const_name "cprod_fun"}),
-                 (@{type_name "u"}, @{const_name "u_fun"})];
+    Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
+                 (@{type_name "++"}, @{const_name "ssum_map"}),
+                 (@{type_name "**"}, @{const_name "sprod_map"}),
+                 (@{type_name "*"}, @{const_name "cprod_map"}),
+                 (@{type_name "u"}, @{const_name "u_map"})];
 
 fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
 and copy r (DatatypeAux.DtRec i) = r i
diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 05 11:47:00 2009 -0800
@@ -589,7 +589,7 @@
   let
     val _ = trace " Proving copy_strict...";
     val goal = mk_trp (strict (dc_copy `% "f"));
-    val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts};
+    val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
     val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
   in pg [ax_copy_def] goal (K tacs) end;
 
@@ -604,9 +604,9 @@
       val rhs = con_app2 con one_rhs args;
       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
       val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
-      val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
+      val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
       fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
-      val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
+      val rules = [ax_abs_iso] @ @{thms domain_map_simps};
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
     in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 in
diff -r 3496616b2171 -r b4210cc3ac97 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Up.thy	Thu Nov 05 11:47:00 2009 -0800
@@ -290,6 +290,43 @@
 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
 by (cases x, simp_all)
 
+subsection {* Map function for lifted cpo *}
+
+definition
+  u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
+where
+  "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
+
+lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
+unfolding u_map_def by simp
+
+lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
+unfolding u_map_def by simp
+
+lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
+apply default
+apply (case_tac x, simp, simp add: ep_pair.e_inverse)
+apply (case_tac y, simp, simp add: ep_pair.e_p_below)
+done
+
+lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
+apply default
+apply (case_tac x, simp, simp add: deflation.idem)
+apply (case_tac x, simp, simp add: deflation.below)
+done
+
+lemma finite_deflation_u_map:
+  assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
+proof (intro finite_deflation.intro finite_deflation_axioms.intro)
+  interpret d: finite_deflation d by fact
+  have "deflation d" by fact
+  thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
+  have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
+    by (rule subsetI, case_tac x, simp_all)
+  thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
+    by (rule finite_subset, simp add: d.finite_fixes)
+qed
+
 subsection {* Lifted cpo is a bifinite domain *}
 
 instantiation u :: (profinite) bifinite
@@ -297,7 +334,7 @@
 
 definition
   approx_up_def:
-    "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
+    "approx = (\<lambda>n. u_map\<cdot>(approx n))"
 
 instance proof
   fix i :: nat and x :: "'a u"
@@ -305,16 +342,15 @@
     unfolding approx_up_def by simp
   show "(\<Squnion>i. approx i\<cdot>x) = x"
     unfolding approx_up_def
-    by (simp add: lub_distribs eta_cfun)
+    by (induct x, simp, simp add: lub_distribs)
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
     unfolding approx_up_def
-    by (induct x, simp, simp)
-  have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
-        insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
+    by (induct x) simp_all
+  show "finite {x::'a u. approx i\<cdot>x = x}"
     unfolding approx_up_def
-    by (rule subsetI, case_tac x, simp_all)
-  thus "finite {x::'a u. approx i\<cdot>x = x}"
-    by (rule finite_subset, simp add: finite_fixes_approx)
+    by (intro finite_deflation.finite_fixes
+              finite_deflation_u_map
+              finite_deflation_approx)
 qed
 
 end