src/HOL/HOLCF/Map_Functions.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 65380 ae93953746fc
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/HOLCF/Map_Functions.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Map functions for various types\<close>
     6 
     7 theory Map_Functions
     8 imports Deflation Sprod Ssum Sfun Up
     9 begin
    10 
    11 subsection \<open>Map operator for continuous function space\<close>
    12 
    13 default_sort cpo
    14 
    15 definition
    16   cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)"
    17 where
    18   "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))"
    19 
    20 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))"
    21 unfolding cfun_map_def by simp
    22 
    23 lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
    24 unfolding cfun_eq_iff by simp
    25 
    26 lemma cfun_map_map:
    27   "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    28     cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    29 by (rule cfun_eqI) simp
    30 
    31 lemma ep_pair_cfun_map:
    32   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    33   shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
    34 proof
    35   interpret e1p1: ep_pair e1 p1 by fact
    36   interpret e2p2: ep_pair e2 p2 by fact
    37   fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    38     by (simp add: cfun_eq_iff)
    39   fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
    40     apply (rule cfun_belowI, simp)
    41     apply (rule below_trans [OF e2p2.e_p_below])
    42     apply (rule monofun_cfun_arg)
    43     apply (rule e1p1.e_p_below)
    44     done
    45 qed
    46 
    47 lemma deflation_cfun_map:
    48   assumes "deflation d1" and "deflation d2"
    49   shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
    50 proof
    51   interpret d1: deflation d1 by fact
    52   interpret d2: deflation d2 by fact
    53   fix f
    54   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
    55     by (simp add: cfun_eq_iff d1.idem d2.idem)
    56   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
    57     apply (rule cfun_belowI, simp)
    58     apply (rule below_trans [OF d2.below])
    59     apply (rule monofun_cfun_arg)
    60     apply (rule d1.below)
    61     done
    62 qed
    63 
    64 lemma finite_range_cfun_map:
    65   assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
    66   assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
    67   shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
    68 proof (rule finite_imageD)
    69   let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
    70   show "finite (?f ` range ?h)"
    71   proof (rule finite_subset)
    72     let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
    73     show "?f ` range ?h \<subseteq> ?B"
    74       by clarsimp
    75     show "finite ?B"
    76       by (simp add: a b)
    77   qed
    78   show "inj_on ?f (range ?h)"
    79   proof (rule inj_onI, rule cfun_eqI, clarsimp)
    80     fix x f g
    81     assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    82     hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    83       by (rule equalityD1)
    84     hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
    85       by (simp add: subset_eq)
    86     then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
    87       by (rule rangeE)
    88     thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
    89       by clarsimp
    90   qed
    91 qed
    92 
    93 lemma finite_deflation_cfun_map:
    94   assumes "finite_deflation d1" and "finite_deflation d2"
    95   shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
    96 proof (rule finite_deflation_intro)
    97   interpret d1: finite_deflation d1 by fact
    98   interpret d2: finite_deflation d2 by fact
    99   have "deflation d1" and "deflation d2" by fact+
   100   thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
   101   have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
   102     using d1.finite_range d2.finite_range
   103     by (rule finite_range_cfun_map)
   104   thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   105     by (rule finite_range_imp_finite_fixes)
   106 qed
   107 
   108 text \<open>Finite deflations are compact elements of the function space\<close>
   109 
   110 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
   111 apply (frule finite_deflation_imp_deflation)
   112 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
   113 apply (simp add: cfun_map_def deflation.idem eta_cfun)
   114 apply (rule finite_deflation.compact)
   115 apply (simp only: finite_deflation_cfun_map)
   116 done
   117 
   118 subsection \<open>Map operator for product type\<close>
   119 
   120 definition
   121   prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
   122 where
   123   "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
   124 
   125 lemma prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
   126 unfolding prod_map_def by simp
   127 
   128 lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID"
   129 unfolding cfun_eq_iff by auto
   130 
   131 lemma prod_map_map:
   132   "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) =
   133     prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   134 by (induct p) simp
   135 
   136 lemma ep_pair_prod_map:
   137   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   138   shows "ep_pair (prod_map\<cdot>e1\<cdot>e2) (prod_map\<cdot>p1\<cdot>p2)"
   139 proof
   140   interpret e1p1: ep_pair e1 p1 by fact
   141   interpret e2p2: ep_pair e2 p2 by fact
   142   fix x show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
   143     by (induct x) simp
   144   fix y show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
   145     by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
   146 qed
   147 
   148 lemma deflation_prod_map:
   149   assumes "deflation d1" and "deflation d2"
   150   shows "deflation (prod_map\<cdot>d1\<cdot>d2)"
   151 proof
   152   interpret d1: deflation d1 by fact
   153   interpret d2: deflation d2 by fact
   154   fix x
   155   show "prod_map\<cdot>d1\<cdot>d2\<cdot>(prod_map\<cdot>d1\<cdot>d2\<cdot>x) = prod_map\<cdot>d1\<cdot>d2\<cdot>x"
   156     by (induct x) (simp add: d1.idem d2.idem)
   157   show "prod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   158     by (induct x) (simp add: d1.below d2.below)
   159 qed
   160 
   161 lemma finite_deflation_prod_map:
   162   assumes "finite_deflation d1" and "finite_deflation d2"
   163   shows "finite_deflation (prod_map\<cdot>d1\<cdot>d2)"
   164 proof (rule finite_deflation_intro)
   165   interpret d1: finite_deflation d1 by fact
   166   interpret d2: finite_deflation d2 by fact
   167   have "deflation d1" and "deflation d2" by fact+
   168   thus "deflation (prod_map\<cdot>d1\<cdot>d2)" by (rule deflation_prod_map)
   169   have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
   170     by clarsimp
   171   thus "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
   172     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   173 qed
   174 
   175 subsection \<open>Map function for lifted cpo\<close>
   176 
   177 definition
   178   u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
   179 where
   180   "u_map = (\<Lambda> f. fup\<cdot>(up oo f))"
   181 
   182 lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>"
   183 unfolding u_map_def by simp
   184 
   185 lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
   186 unfolding u_map_def by simp
   187 
   188 lemma u_map_ID: "u_map\<cdot>ID = ID"
   189 unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
   190 
   191 lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
   192 by (induct p) simp_all
   193 
   194 lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g"
   195 by (simp add: cfcomp1 u_map_map eta_cfun)
   196 
   197 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
   198 apply standard
   199 apply (case_tac x, simp, simp add: ep_pair.e_inverse)
   200 apply (case_tac y, simp, simp add: ep_pair.e_p_below)
   201 done
   202 
   203 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
   204 apply standard
   205 apply (case_tac x, simp, simp add: deflation.idem)
   206 apply (case_tac x, simp, simp add: deflation.below)
   207 done
   208 
   209 lemma finite_deflation_u_map:
   210   assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)"
   211 proof (rule finite_deflation_intro)
   212   interpret d: finite_deflation d by fact
   213   have "deflation d" by fact
   214   thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map)
   215   have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})"
   216     by (rule subsetI, case_tac x, simp_all)
   217   thus "finite {x. u_map\<cdot>d\<cdot>x = x}"
   218     by (rule finite_subset, simp add: d.finite_fixes)
   219 qed
   220 
   221 subsection \<open>Map function for strict products\<close>
   222 
   223 default_sort pcpo
   224 
   225 definition
   226   sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd"
   227 where
   228   "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))"
   229 
   230 lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>"
   231 unfolding sprod_map_def by simp
   232 
   233 lemma sprod_map_spair [simp]:
   234   "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
   235 by (simp add: sprod_map_def)
   236 
   237 lemma sprod_map_spair':
   238   "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
   239 by (cases "x = \<bottom> \<or> y = \<bottom>") auto
   240 
   241 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
   242 unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
   243 
   244 lemma sprod_map_map:
   245   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
   246     sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
   247      sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   248 apply (induct p, simp)
   249 apply (case_tac "f2\<cdot>x = \<bottom>", simp)
   250 apply (case_tac "g2\<cdot>y = \<bottom>", simp)
   251 apply simp
   252 done
   253 
   254 lemma ep_pair_sprod_map:
   255   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   256   shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)"
   257 proof
   258   interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
   259   interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
   260   fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
   261     by (induct x) simp_all
   262   fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
   263     apply (induct y, simp)
   264     apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
   265     apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
   266     done
   267 qed
   268 
   269 lemma deflation_sprod_map:
   270   assumes "deflation d1" and "deflation d2"
   271   shows "deflation (sprod_map\<cdot>d1\<cdot>d2)"
   272 proof
   273   interpret d1: deflation d1 by fact
   274   interpret d2: deflation d2 by fact
   275   fix x
   276   show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
   277     apply (induct x, simp)
   278     apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
   279     apply (simp add: d1.idem d2.idem)
   280     done
   281   show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   282     apply (induct x, simp)
   283     apply (simp add: monofun_cfun d1.below d2.below)
   284     done
   285 qed
   286 
   287 lemma finite_deflation_sprod_map:
   288   assumes "finite_deflation d1" and "finite_deflation d2"
   289   shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)"
   290 proof (rule finite_deflation_intro)
   291   interpret d1: finite_deflation d1 by fact
   292   interpret d2: finite_deflation d2 by fact
   293   have "deflation d1" and "deflation d2" by fact+
   294   thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map)
   295   have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom>
   296         ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))"
   297     by (rule subsetI, case_tac x, auto simp add: spair_eq_iff)
   298   thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
   299     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   300 qed
   301 
   302 subsection \<open>Map function for strict sums\<close>
   303 
   304 definition
   305   ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
   306 where
   307   "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))"
   308 
   309 lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
   310 unfolding ssum_map_def by simp
   311 
   312 lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
   313 unfolding ssum_map_def by simp
   314 
   315 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
   316 unfolding ssum_map_def by simp
   317 
   318 lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
   319 by (cases "x = \<bottom>") simp_all
   320 
   321 lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
   322 by (cases "x = \<bottom>") simp_all
   323 
   324 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
   325 unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
   326 
   327 lemma ssum_map_map:
   328   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
   329     ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
   330      ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   331 apply (induct p, simp)
   332 apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
   333 apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
   334 done
   335 
   336 lemma ep_pair_ssum_map:
   337   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   338   shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)"
   339 proof
   340   interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact
   341   interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact
   342   fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
   343     by (induct x) simp_all
   344   fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
   345     apply (induct y, simp)
   346     apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
   347     apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
   348     done
   349 qed
   350 
   351 lemma deflation_ssum_map:
   352   assumes "deflation d1" and "deflation d2"
   353   shows "deflation (ssum_map\<cdot>d1\<cdot>d2)"
   354 proof
   355   interpret d1: deflation d1 by fact
   356   interpret d2: deflation d2 by fact
   357   fix x
   358   show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
   359     apply (induct x, simp)
   360     apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
   361     apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
   362     done
   363   show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
   364     apply (induct x, simp)
   365     apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
   366     apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
   367     done
   368 qed
   369 
   370 lemma finite_deflation_ssum_map:
   371   assumes "finite_deflation d1" and "finite_deflation d2"
   372   shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)"
   373 proof (rule finite_deflation_intro)
   374   interpret d1: finite_deflation d1 by fact
   375   interpret d2: finite_deflation d2 by fact
   376   have "deflation d1" and "deflation d2" by fact+
   377   thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map)
   378   have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq>
   379         (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union>
   380         (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}"
   381     by (rule subsetI, case_tac x, simp_all)
   382   thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}"
   383     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   384 qed
   385 
   386 subsection \<open>Map operator for strict function space\<close>
   387 
   388 definition
   389   sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
   390 where
   391   "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
   392 
   393 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
   394   unfolding sfun_map_def
   395   by (simp add: cfun_map_ID cfun_eq_iff)
   396 
   397 lemma sfun_map_map:
   398   assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
   399   "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
   400     sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   401 unfolding sfun_map_def
   402 by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
   403 
   404 lemma ep_pair_sfun_map:
   405   assumes 1: "ep_pair e1 p1"
   406   assumes 2: "ep_pair e2 p2"
   407   shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)"
   408 proof
   409   interpret e1p1: pcpo_ep_pair e1 p1
   410     unfolding pcpo_ep_pair_def by fact
   411   interpret e2p2: pcpo_ep_pair e2 p2
   412     unfolding pcpo_ep_pair_def by fact
   413   fix f show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
   414     unfolding sfun_map_def
   415     apply (simp add: sfun_eq_iff strictify_cancel)
   416     apply (rule ep_pair.e_inverse)
   417     apply (rule ep_pair_cfun_map [OF 1 2])
   418     done
   419   fix g show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
   420     unfolding sfun_map_def
   421     apply (simp add: sfun_below_iff strictify_cancel)
   422     apply (rule ep_pair.e_p_below)
   423     apply (rule ep_pair_cfun_map [OF 1 2])
   424     done
   425 qed
   426 
   427 lemma deflation_sfun_map:
   428   assumes 1: "deflation d1"
   429   assumes 2: "deflation d2"
   430   shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
   431 apply (simp add: sfun_map_def)
   432 apply (rule deflation.intro)
   433 apply simp
   434 apply (subst strictify_cancel)
   435 apply (simp add: cfun_map_def deflation_strict 1 2)
   436 apply (simp add: cfun_map_def deflation.idem 1 2)
   437 apply (simp add: sfun_below_iff)
   438 apply (subst strictify_cancel)
   439 apply (simp add: cfun_map_def deflation_strict 1 2)
   440 apply (rule deflation.below)
   441 apply (rule deflation_cfun_map [OF 1 2])
   442 done
   443 
   444 lemma finite_deflation_sfun_map:
   445   assumes 1: "finite_deflation d1"
   446   assumes 2: "finite_deflation d2"
   447   shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)"
   448 proof (intro finite_deflation_intro)
   449   interpret d1: finite_deflation d1 by fact
   450   interpret d2: finite_deflation d2 by fact
   451   have "deflation d1" and "deflation d2" by fact+
   452   thus "deflation (sfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_sfun_map)
   453   from 1 2 have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
   454     by (rule finite_deflation_cfun_map)
   455   then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   456     by (rule finite_deflation.finite_fixes)
   457   moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)"
   458     by (rule inj_onI, simp add: sfun_eq_iff)
   459   ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})"
   460     by (rule finite_vimageI)
   461   then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
   462     unfolding sfun_map_def sfun_eq_iff
   463     by (simp add: strictify_cancel
   464          deflation_strict \<open>deflation d1\<close> \<open>deflation d2\<close>)
   465 qed
   466 
   467 end