--- a/src/HOLCF/Map_Functions.thy Wed Nov 17 06:49:23 2010 -0800
+++ b/src/HOLCF/Map_Functions.thy Wed Nov 17 08:47:58 2010 -0800
@@ -380,4 +380,85 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
+subsection {* Map operator for strict function space *}
+
+definition
+ sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
+where
+ "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
+
+lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
+ unfolding sfun_map_def
+ by (simp add: cfun_map_ID cfun_eq_iff)
+
+lemma sfun_map_map:
+ assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
+ "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
+ sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
+unfolding sfun_map_def
+by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
+
+lemma ep_pair_sfun_map:
+ assumes 1: "ep_pair e1 p1"
+ assumes 2: "ep_pair e2 p2"
+ shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<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 f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
+ unfolding sfun_map_def
+ apply (simp add: sfun_eq_iff strictify_cancel)
+ apply (rule ep_pair.e_inverse)
+ apply (rule ep_pair_cfun_map [OF 1 2])
+ done
+ fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
+ unfolding sfun_map_def
+ apply (simp add: sfun_below_iff strictify_cancel)
+ apply (rule ep_pair.e_p_below)
+ apply (rule ep_pair_cfun_map [OF 1 2])
+ done
+qed
+
+lemma deflation_sfun_map:
+ assumes 1: "deflation d1"
+ assumes 2: "deflation d2"
+ shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
+apply (simp add: sfun_map_def)
+apply (rule deflation.intro)
+apply simp
+apply (subst strictify_cancel)
+apply (simp add: cfun_map_def deflation_strict 1 2)
+apply (simp add: cfun_map_def deflation.idem 1 2)
+apply (simp add: sfun_below_iff)
+apply (subst strictify_cancel)
+apply (simp add: cfun_map_def deflation_strict 1 2)
+apply (rule deflation.below)
+apply (rule deflation_cfun_map [OF 1 2])
+done
+
+lemma finite_deflation_sfun_map:
+ assumes 1: "finite_deflation d1"
+ assumes 2: "finite_deflation d2"
+ shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
+proof (intro finite_deflation_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 (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
+ from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
+ by (rule finite_deflation_cfun_map)
+ then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ by (rule finite_deflation.finite_fixes)
+ moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
+ by (rule inj_onI, simp add: sfun_eq_iff)
+ ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
+ by (rule finite_vimageI)
+ then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
+ unfolding sfun_map_def sfun_eq_iff
+ by (simp add: strictify_cancel
+ deflation_strict `deflation d1` `deflation d2`)
+qed
+
end