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