src/HOLCF/Map_Functions.thy

     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 {* 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