src/HOLCF/Deflation.thy
 author huffman Mon Oct 11 21:35:31 2010 -0700 (2010-10-11) changeset 40002 c5b5f7a3a3b1 parent 39985 310f98585107 child 40321 d065b195ec89 permissions -rw-r--r--
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
```     1 (*  Title:      HOLCF/Deflation.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* Continuous deflations and ep-pairs *}
```
```     6
```
```     7 theory Deflation
```
```     8 imports Cfun
```
```     9 begin
```
```    10
```
```    11 default_sort cpo
```
```    12
```
```    13 subsection {* Continuous deflations *}
```
```    14
```
```    15 locale deflation =
```
```    16   fixes d :: "'a \<rightarrow> 'a"
```
```    17   assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
```
```    18   assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
```
```    19 begin
```
```    20
```
```    21 lemma below_ID: "d \<sqsubseteq> ID"
```
```    22 by (rule cfun_belowI, simp add: below)
```
```    23
```
```    24 text {* The set of fixed points is the same as the range. *}
```
```    25
```
```    26 lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
```
```    27 by (auto simp add: eq_sym_conv idem)
```
```    28
```
```    29 lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
```
```    30 by (auto simp add: eq_sym_conv idem)
```
```    31
```
```    32 text {*
```
```    33   The pointwise ordering on deflation functions coincides with
```
```    34   the subset ordering of their sets of fixed-points.
```
```    35 *}
```
```    36
```
```    37 lemma belowI:
```
```    38   assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
```
```    39 proof (rule cfun_belowI)
```
```    40   fix x
```
```    41   from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
```
```    42   also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
```
```    43   finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
```
```    44 qed
```
```    45
```
```    46 lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
```
```    47 proof (rule below_antisym)
```
```    48   from below show "d\<cdot>x \<sqsubseteq> x" .
```
```    49 next
```
```    50   assume "f \<sqsubseteq> d"
```
```    51   hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
```
```    52   also assume "f\<cdot>x = x"
```
```    53   finally show "x \<sqsubseteq> d\<cdot>x" .
```
```    54 qed
```
```    55
```
```    56 end
```
```    57
```
```    58 lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
```
```    59 by (rule deflation.below [THEN UU_I])
```
```    60
```
```    61 lemma adm_deflation: "adm (\<lambda>d. deflation d)"
```
```    62 by (simp add: deflation_def)
```
```    63
```
```    64 lemma deflation_ID: "deflation ID"
```
```    65 by (simp add: deflation.intro)
```
```    66
```
```    67 lemma deflation_UU: "deflation \<bottom>"
```
```    68 by (simp add: deflation.intro)
```
```    69
```
```    70 lemma deflation_below_iff:
```
```    71   "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
```
```    72  apply safe
```
```    73   apply (simp add: deflation.belowD)
```
```    74  apply (simp add: deflation.belowI)
```
```    75 done
```
```    76
```
```    77 text {*
```
```    78   The composition of two deflations is equal to
```
```    79   the lesser of the two (if they are comparable).
```
```    80 *}
```
```    81
```
```    82 lemma deflation_below_comp1:
```
```    83   assumes "deflation f"
```
```    84   assumes "deflation g"
```
```    85   shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
```
```    86 proof (rule below_antisym)
```
```    87   interpret g: deflation g by fact
```
```    88   from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
```
```    89 next
```
```    90   interpret f: deflation f by fact
```
```    91   assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
```
```    92   hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
```
```    93   also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
```
```    94   finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
```
```    95 qed
```
```    96
```
```    97 lemma deflation_below_comp2:
```
```    98   "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
```
```    99 by (simp only: deflation.belowD deflation.idem)
```
```   100
```
```   101
```
```   102 subsection {* Deflations with finite range *}
```
```   103
```
```   104 lemma finite_range_imp_finite_fixes:
```
```   105   "finite (range f) \<Longrightarrow> finite {x. f x = x}"
```
```   106 proof -
```
```   107   have "{x. f x = x} \<subseteq> range f"
```
```   108     by (clarify, erule subst, rule rangeI)
```
```   109   moreover assume "finite (range f)"
```
```   110   ultimately show "finite {x. f x = x}"
```
```   111     by (rule finite_subset)
```
```   112 qed
```
```   113
```
```   114 locale finite_deflation = deflation +
```
```   115   assumes finite_fixes: "finite {x. d\<cdot>x = x}"
```
```   116 begin
```
```   117
```
```   118 lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
```
```   119 by (simp add: range_eq_fixes finite_fixes)
```
```   120
```
```   121 lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
```
```   122 by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
```
```   123
```
```   124 lemma compact: "compact (d\<cdot>x)"
```
```   125 proof (rule compactI2)
```
```   126   fix Y :: "nat \<Rightarrow> 'a"
```
```   127   assume Y: "chain Y"
```
```   128   have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
```
```   129   proof (rule finite_range_imp_finch)
```
```   130     show "chain (\<lambda>i. d\<cdot>(Y i))"
```
```   131       using Y by simp
```
```   132     have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
```
```   133       by clarsimp
```
```   134     thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
```
```   135       using finite_range by (rule finite_subset)
```
```   136   qed
```
```   137   hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
```
```   138     by (simp add: finite_chain_def maxinch_is_thelub Y)
```
```   139   then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
```
```   140
```
```   141   assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
```
```   142   hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
```
```   143     by (rule monofun_cfun_arg)
```
```   144   hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
```
```   145     by (simp add: contlub_cfun_arg Y idem)
```
```   146   hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
```
```   147     using j by simp
```
```   148   hence "d\<cdot>x \<sqsubseteq> Y j"
```
```   149     using below by (rule below_trans)
```
```   150   thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
```
```   151 qed
```
```   152
```
```   153 end
```
```   154
```
```   155 lemma finite_deflation_intro:
```
```   156   "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
```
```   157 by (intro finite_deflation.intro finite_deflation_axioms.intro)
```
```   158
```
```   159 lemma finite_deflation_imp_deflation:
```
```   160   "finite_deflation d \<Longrightarrow> deflation d"
```
```   161 unfolding finite_deflation_def by simp
```
```   162
```
```   163 lemma finite_deflation_UU: "finite_deflation \<bottom>"
```
```   164 by default simp_all
```
```   165
```
```   166
```
```   167 subsection {* Continuous embedding-projection pairs *}
```
```   168
```
```   169 locale ep_pair =
```
```   170   fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
```
```   171   assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
```
```   172   and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
```
```   173 begin
```
```   174
```
```   175 lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
```
```   176 proof
```
```   177   assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
```
```   178   hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
```
```   179   thus "x \<sqsubseteq> y" by simp
```
```   180 next
```
```   181   assume "x \<sqsubseteq> y"
```
```   182   thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
```
```   183 qed
```
```   184
```
```   185 lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
```
```   186 unfolding po_eq_conv e_below_iff ..
```
```   187
```
```   188 lemma p_eq_iff:
```
```   189   "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
```
```   190 by (safe, erule subst, erule subst, simp)
```
```   191
```
```   192 lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
```
```   193 by (auto, rule exI, erule sym)
```
```   194
```
```   195 lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
```
```   196 proof
```
```   197   assume "e\<cdot>x \<sqsubseteq> y"
```
```   198   then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
```
```   199   then show "x \<sqsubseteq> p\<cdot>y" by simp
```
```   200 next
```
```   201   assume "x \<sqsubseteq> p\<cdot>y"
```
```   202   then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
```
```   203   then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
```
```   204 qed
```
```   205
```
```   206 lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
```
```   207 proof -
```
```   208   assume "compact (e\<cdot>x)"
```
```   209   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
```
```   210   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
```
```   211   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
```
```   212   thus "compact x" by (rule compactI)
```
```   213 qed
```
```   214
```
```   215 lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
```
```   216 proof -
```
```   217   assume "compact x"
```
```   218   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
```
```   219   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
```
```   220   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
```
```   221   thus "compact (e\<cdot>x)" by (rule compactI)
```
```   222 qed
```
```   223
```
```   224 lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
```
```   225 by (rule iffI [OF compact_e_rev compact_e])
```
```   226
```
```   227 text {* Deflations from ep-pairs *}
```
```   228
```
```   229 lemma deflation_e_p: "deflation (e oo p)"
```
```   230 by (simp add: deflation.intro e_p_below)
```
```   231
```
```   232 lemma deflation_e_d_p:
```
```   233   assumes "deflation d"
```
```   234   shows "deflation (e oo d oo p)"
```
```   235 proof
```
```   236   interpret deflation d by fact
```
```   237   fix x :: 'b
```
```   238   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
```
```   239     by (simp add: idem)
```
```   240   show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
```
```   241     by (simp add: e_below_iff_below_p below)
```
```   242 qed
```
```   243
```
```   244 lemma finite_deflation_e_d_p:
```
```   245   assumes "finite_deflation d"
```
```   246   shows "finite_deflation (e oo d oo p)"
```
```   247 proof
```
```   248   interpret finite_deflation d by fact
```
```   249   fix x :: 'b
```
```   250   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
```
```   251     by (simp add: idem)
```
```   252   show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
```
```   253     by (simp add: e_below_iff_below_p below)
```
```   254   have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
```
```   255     by (simp add: finite_image)
```
```   256   hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
```
```   257     by (simp add: image_image)
```
```   258   thus "finite {x. (e oo d oo p)\<cdot>x = x}"
```
```   259     by (rule finite_range_imp_finite_fixes)
```
```   260 qed
```
```   261
```
```   262 lemma deflation_p_d_e:
```
```   263   assumes "deflation d"
```
```   264   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
```
```   265   shows "deflation (p oo d oo e)"
```
```   266 proof -
```
```   267   interpret d: deflation d by fact
```
```   268   {
```
```   269     fix x
```
```   270     have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
```
```   271       by (rule d.below)
```
```   272     hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
```
```   273       by (rule monofun_cfun_arg)
```
```   274     hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
```
```   275       by simp
```
```   276   }
```
```   277   note p_d_e_below = this
```
```   278   show ?thesis
```
```   279   proof
```
```   280     fix x
```
```   281     show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
```
```   282       by (rule p_d_e_below)
```
```   283   next
```
```   284     fix x
```
```   285     show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
```
```   286     proof (rule below_antisym)
```
```   287       show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
```
```   288         by (rule p_d_e_below)
```
```   289       have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
```
```   290         by (intro monofun_cfun_arg d)
```
```   291       hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
```
```   292         by (simp only: d.idem)
```
```   293       thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
```
```   294         by simp
```
```   295     qed
```
```   296   qed
```
```   297 qed
```
```   298
```
```   299 lemma finite_deflation_p_d_e:
```
```   300   assumes "finite_deflation d"
```
```   301   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
```
```   302   shows "finite_deflation (p oo d oo e)"
```
```   303 proof -
```
```   304   interpret d: finite_deflation d by fact
```
```   305   show ?thesis
```
```   306   proof (rule finite_deflation_intro)
```
```   307     have "deflation d" ..
```
```   308     thus "deflation (p oo d oo e)"
```
```   309       using d by (rule deflation_p_d_e)
```
```   310   next
```
```   311     have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
```
```   312       by (rule d.finite_image)
```
```   313     hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
```
```   314       by (rule finite_imageI)
```
```   315     hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
```
```   316       by (simp add: image_image)
```
```   317     thus "finite {x. (p oo d oo e)\<cdot>x = x}"
```
```   318       by (rule finite_range_imp_finite_fixes)
```
```   319   qed
```
```   320 qed
```
```   321
```
```   322 end
```
```   323
```
```   324 subsection {* Uniqueness of ep-pairs *}
```
```   325
```
```   326 lemma ep_pair_unique_e_lemma:
```
```   327   assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
```
```   328   shows "e1 \<sqsubseteq> e2"
```
```   329 proof (rule cfun_belowI)
```
```   330   fix x
```
```   331   have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
```
```   332     by (rule ep_pair.e_p_below [OF 1])
```
```   333   thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
```
```   334     by (simp only: ep_pair.e_inverse [OF 2])
```
```   335 qed
```
```   336
```
```   337 lemma ep_pair_unique_e:
```
```   338   "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
```
```   339 by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
```
```   340
```
```   341 lemma ep_pair_unique_p_lemma:
```
```   342   assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
```
```   343   shows "p1 \<sqsubseteq> p2"
```
```   344 proof (rule cfun_belowI)
```
```   345   fix x
```
```   346   have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
```
```   347     by (rule ep_pair.e_p_below [OF 1])
```
```   348   hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
```
```   349     by (rule monofun_cfun_arg)
```
```   350   thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
```
```   351     by (simp only: ep_pair.e_inverse [OF 2])
```
```   352 qed
```
```   353
```
```   354 lemma ep_pair_unique_p:
```
```   355   "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
```
```   356 by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
```
```   357
```
```   358 subsection {* Composing ep-pairs *}
```
```   359
```
```   360 lemma ep_pair_ID_ID: "ep_pair ID ID"
```
```   361 by default simp_all
```
```   362
```
```   363 lemma ep_pair_comp:
```
```   364   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
```
```   365   shows "ep_pair (e2 oo e1) (p1 oo p2)"
```
```   366 proof
```
```   367   interpret ep1: ep_pair e1 p1 by fact
```
```   368   interpret ep2: ep_pair e2 p2 by fact
```
```   369   fix x y
```
```   370   show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
```
```   371     by simp
```
```   372   have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
```
```   373     by (rule ep1.e_p_below)
```
```   374   hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
```
```   375     by (rule monofun_cfun_arg)
```
```   376   also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
```
```   377     by (rule ep2.e_p_below)
```
```   378   finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
```
```   379     by simp
```
```   380 qed
```
```   381
```
```   382 locale pcpo_ep_pair = ep_pair +
```
```   383   constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
```
```   384   constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
```
```   385 begin
```
```   386
```
```   387 lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
```
```   388 proof -
```
```   389   have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
```
```   390   hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
```
```   391   also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
```
```   392   finally show "e\<cdot>\<bottom> = \<bottom>" by simp
```
```   393 qed
```
```   394
```
```   395 lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
```
```   396 by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
```
```   397
```
```   398 lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
```
```   399 by simp
```
```   400
```
```   401 lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
```
```   402 by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
```
```   403
```
```   404 lemmas stricts = e_strict p_strict
```
```   405
```
```   406 end
```
```   407
```
```   408 subsection {* Map operator for continuous functions *}
```
```   409
```
```   410 lemma ep_pair_cfun_map:
```
```   411   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
```
```   412   shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
```
```   413 proof
```
```   414   interpret e1p1: ep_pair e1 p1 by fact
```
```   415   interpret e2p2: ep_pair e2 p2 by fact
```
```   416   fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
```
```   417     by (simp add: cfun_eq_iff)
```
```   418   fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
```
```   419     apply (rule cfun_belowI, simp)
```
```   420     apply (rule below_trans [OF e2p2.e_p_below])
```
```   421     apply (rule monofun_cfun_arg)
```
```   422     apply (rule e1p1.e_p_below)
```
```   423     done
```
```   424 qed
```
```   425
```
```   426 lemma deflation_cfun_map:
```
```   427   assumes "deflation d1" and "deflation d2"
```
```   428   shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
```
```   429 proof
```
```   430   interpret d1: deflation d1 by fact
```
```   431   interpret d2: deflation d2 by fact
```
```   432   fix f
```
```   433   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
```
```   434     by (simp add: cfun_eq_iff d1.idem d2.idem)
```
```   435   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
```
```   436     apply (rule cfun_belowI, simp)
```
```   437     apply (rule below_trans [OF d2.below])
```
```   438     apply (rule monofun_cfun_arg)
```
```   439     apply (rule d1.below)
```
```   440     done
```
```   441 qed
```
```   442
```
```   443 lemma finite_range_cfun_map:
```
```   444   assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
```
```   445   assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
```
```   446   shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
```
```   447 proof (rule finite_imageD)
```
```   448   let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
```
```   449   show "finite (?f ` range ?h)"
```
```   450   proof (rule finite_subset)
```
```   451     let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
```
```   452     show "?f ` range ?h \<subseteq> ?B"
```
```   453       by clarsimp
```
```   454     show "finite ?B"
```
```   455       by (simp add: a b)
```
```   456   qed
```
```   457   show "inj_on ?f (range ?h)"
```
```   458   proof (rule inj_onI, rule cfun_eqI, clarsimp)
```
```   459     fix x f g
```
```   460     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))))"
```
```   461     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))))"
```
```   462       by (rule equalityD1)
```
```   463     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))))"
```
```   464       by (simp add: subset_eq)
```
```   465     then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
```
```   466       by (rule rangeE)
```
```   467     thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
```
```   468       by clarsimp
```
```   469   qed
```
```   470 qed
```
```   471
```
```   472 lemma finite_deflation_cfun_map:
```
```   473   assumes "finite_deflation d1" and "finite_deflation d2"
```
```   474   shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
```
```   475 proof (rule finite_deflation_intro)
```
```   476   interpret d1: finite_deflation d1 by fact
```
```   477   interpret d2: finite_deflation d2 by fact
```
```   478   have "deflation d1" and "deflation d2" by fact+
```
```   479   thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
```
```   480   have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
```
```   481     using d1.finite_range d2.finite_range
```
```   482     by (rule finite_range_cfun_map)
```
```   483   thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
```
```   484     by (rule finite_range_imp_finite_fixes)
```
```   485 qed
```
```   486
```
```   487 text {* Finite deflations are compact elements of the function space *}
```
```   488
```
```   489 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
```
```   490 apply (frule finite_deflation_imp_deflation)
```
```   491 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
```
```   492 apply (simp add: cfun_map_def deflation.idem eta_cfun)
```
```   493 apply (rule finite_deflation.compact)
```
```   494 apply (simp only: finite_deflation_cfun_map)
```
```   495 done
```
```   496
```
```   497 end
```