src/HOL/HOLCF/Deflation.thy
changeset 40774 0437dbc127b3
parent 40502 8e92772bc0e8
child 41182 717404c7d59a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Deflation.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,408 @@
     1.4 +(*  Title:      HOLCF/Deflation.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Continuous deflations and ep-pairs *}
     1.9 +
    1.10 +theory Deflation
    1.11 +imports Plain_HOLCF
    1.12 +begin
    1.13 +
    1.14 +default_sort cpo
    1.15 +
    1.16 +subsection {* Continuous deflations *}
    1.17 +
    1.18 +locale deflation =
    1.19 +  fixes d :: "'a \<rightarrow> 'a"
    1.20 +  assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
    1.21 +  assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
    1.22 +begin
    1.23 +
    1.24 +lemma below_ID: "d \<sqsubseteq> ID"
    1.25 +by (rule cfun_belowI, simp add: below)
    1.26 +
    1.27 +text {* The set of fixed points is the same as the range. *}
    1.28 +
    1.29 +lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
    1.30 +by (auto simp add: eq_sym_conv idem)
    1.31 +
    1.32 +lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
    1.33 +by (auto simp add: eq_sym_conv idem)
    1.34 +
    1.35 +text {*
    1.36 +  The pointwise ordering on deflation functions coincides with
    1.37 +  the subset ordering of their sets of fixed-points.
    1.38 +*}
    1.39 +
    1.40 +lemma belowI:
    1.41 +  assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
    1.42 +proof (rule cfun_belowI)
    1.43 +  fix x
    1.44 +  from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
    1.45 +  also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
    1.46 +  finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
    1.47 +qed
    1.48 +
    1.49 +lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
    1.50 +proof (rule below_antisym)
    1.51 +  from below show "d\<cdot>x \<sqsubseteq> x" .
    1.52 +next
    1.53 +  assume "f \<sqsubseteq> d"
    1.54 +  hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
    1.55 +  also assume "f\<cdot>x = x"
    1.56 +  finally show "x \<sqsubseteq> d\<cdot>x" .
    1.57 +qed
    1.58 +
    1.59 +end
    1.60 +
    1.61 +lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
    1.62 +by (rule deflation.below [THEN UU_I])
    1.63 +
    1.64 +lemma adm_deflation: "adm (\<lambda>d. deflation d)"
    1.65 +by (simp add: deflation_def)
    1.66 +
    1.67 +lemma deflation_ID: "deflation ID"
    1.68 +by (simp add: deflation.intro)
    1.69 +
    1.70 +lemma deflation_UU: "deflation \<bottom>"
    1.71 +by (simp add: deflation.intro)
    1.72 +
    1.73 +lemma deflation_below_iff:
    1.74 +  "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
    1.75 + apply safe
    1.76 +  apply (simp add: deflation.belowD)
    1.77 + apply (simp add: deflation.belowI)
    1.78 +done
    1.79 +
    1.80 +text {*
    1.81 +  The composition of two deflations is equal to
    1.82 +  the lesser of the two (if they are comparable).
    1.83 +*}
    1.84 +
    1.85 +lemma deflation_below_comp1:
    1.86 +  assumes "deflation f"
    1.87 +  assumes "deflation g"
    1.88 +  shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
    1.89 +proof (rule below_antisym)
    1.90 +  interpret g: deflation g by fact
    1.91 +  from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
    1.92 +next
    1.93 +  interpret f: deflation f by fact
    1.94 +  assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
    1.95 +  hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
    1.96 +  also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
    1.97 +  finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
    1.98 +qed
    1.99 +
   1.100 +lemma deflation_below_comp2:
   1.101 +  "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
   1.102 +by (simp only: deflation.belowD deflation.idem)
   1.103 +
   1.104 +
   1.105 +subsection {* Deflations with finite range *}
   1.106 +
   1.107 +lemma finite_range_imp_finite_fixes:
   1.108 +  "finite (range f) \<Longrightarrow> finite {x. f x = x}"
   1.109 +proof -
   1.110 +  have "{x. f x = x} \<subseteq> range f"
   1.111 +    by (clarify, erule subst, rule rangeI)
   1.112 +  moreover assume "finite (range f)"
   1.113 +  ultimately show "finite {x. f x = x}"
   1.114 +    by (rule finite_subset)
   1.115 +qed
   1.116 +
   1.117 +locale finite_deflation = deflation +
   1.118 +  assumes finite_fixes: "finite {x. d\<cdot>x = x}"
   1.119 +begin
   1.120 +
   1.121 +lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
   1.122 +by (simp add: range_eq_fixes finite_fixes)
   1.123 +
   1.124 +lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
   1.125 +by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
   1.126 +
   1.127 +lemma compact: "compact (d\<cdot>x)"
   1.128 +proof (rule compactI2)
   1.129 +  fix Y :: "nat \<Rightarrow> 'a"
   1.130 +  assume Y: "chain Y"
   1.131 +  have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
   1.132 +  proof (rule finite_range_imp_finch)
   1.133 +    show "chain (\<lambda>i. d\<cdot>(Y i))"
   1.134 +      using Y by simp
   1.135 +    have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
   1.136 +      by clarsimp
   1.137 +    thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
   1.138 +      using finite_range by (rule finite_subset)
   1.139 +  qed
   1.140 +  hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
   1.141 +    by (simp add: finite_chain_def maxinch_is_thelub Y)
   1.142 +  then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
   1.143 +
   1.144 +  assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
   1.145 +  hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
   1.146 +    by (rule monofun_cfun_arg)
   1.147 +  hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
   1.148 +    by (simp add: contlub_cfun_arg Y idem)
   1.149 +  hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
   1.150 +    using j by simp
   1.151 +  hence "d\<cdot>x \<sqsubseteq> Y j"
   1.152 +    using below by (rule below_trans)
   1.153 +  thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
   1.154 +qed
   1.155 +
   1.156 +end
   1.157 +
   1.158 +lemma finite_deflation_intro:
   1.159 +  "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
   1.160 +by (intro finite_deflation.intro finite_deflation_axioms.intro)
   1.161 +
   1.162 +lemma finite_deflation_imp_deflation:
   1.163 +  "finite_deflation d \<Longrightarrow> deflation d"
   1.164 +unfolding finite_deflation_def by simp
   1.165 +
   1.166 +lemma finite_deflation_UU: "finite_deflation \<bottom>"
   1.167 +by default simp_all
   1.168 +
   1.169 +
   1.170 +subsection {* Continuous embedding-projection pairs *}
   1.171 +
   1.172 +locale ep_pair =
   1.173 +  fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
   1.174 +  assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
   1.175 +  and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
   1.176 +begin
   1.177 +
   1.178 +lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
   1.179 +proof
   1.180 +  assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
   1.181 +  hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
   1.182 +  thus "x \<sqsubseteq> y" by simp
   1.183 +next
   1.184 +  assume "x \<sqsubseteq> y"
   1.185 +  thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
   1.186 +qed
   1.187 +
   1.188 +lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
   1.189 +unfolding po_eq_conv e_below_iff ..
   1.190 +
   1.191 +lemma p_eq_iff:
   1.192 +  "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
   1.193 +by (safe, erule subst, erule subst, simp)
   1.194 +
   1.195 +lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
   1.196 +by (auto, rule exI, erule sym)
   1.197 +
   1.198 +lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
   1.199 +proof
   1.200 +  assume "e\<cdot>x \<sqsubseteq> y"
   1.201 +  then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
   1.202 +  then show "x \<sqsubseteq> p\<cdot>y" by simp
   1.203 +next
   1.204 +  assume "x \<sqsubseteq> p\<cdot>y"
   1.205 +  then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
   1.206 +  then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
   1.207 +qed
   1.208 +
   1.209 +lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
   1.210 +proof -
   1.211 +  assume "compact (e\<cdot>x)"
   1.212 +  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
   1.213 +  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   1.214 +  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
   1.215 +  thus "compact x" by (rule compactI)
   1.216 +qed
   1.217 +
   1.218 +lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
   1.219 +proof -
   1.220 +  assume "compact x"
   1.221 +  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
   1.222 +  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   1.223 +  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
   1.224 +  thus "compact (e\<cdot>x)" by (rule compactI)
   1.225 +qed
   1.226 +
   1.227 +lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
   1.228 +by (rule iffI [OF compact_e_rev compact_e])
   1.229 +
   1.230 +text {* Deflations from ep-pairs *}
   1.231 +
   1.232 +lemma deflation_e_p: "deflation (e oo p)"
   1.233 +by (simp add: deflation.intro e_p_below)
   1.234 +
   1.235 +lemma deflation_e_d_p:
   1.236 +  assumes "deflation d"
   1.237 +  shows "deflation (e oo d oo p)"
   1.238 +proof
   1.239 +  interpret deflation d by fact
   1.240 +  fix x :: 'b
   1.241 +  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
   1.242 +    by (simp add: idem)
   1.243 +  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
   1.244 +    by (simp add: e_below_iff_below_p below)
   1.245 +qed
   1.246 +
   1.247 +lemma finite_deflation_e_d_p:
   1.248 +  assumes "finite_deflation d"
   1.249 +  shows "finite_deflation (e oo d oo p)"
   1.250 +proof
   1.251 +  interpret finite_deflation d by fact
   1.252 +  fix x :: 'b
   1.253 +  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
   1.254 +    by (simp add: idem)
   1.255 +  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
   1.256 +    by (simp add: e_below_iff_below_p below)
   1.257 +  have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
   1.258 +    by (simp add: finite_image)
   1.259 +  hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
   1.260 +    by (simp add: image_image)
   1.261 +  thus "finite {x. (e oo d oo p)\<cdot>x = x}"
   1.262 +    by (rule finite_range_imp_finite_fixes)
   1.263 +qed
   1.264 +
   1.265 +lemma deflation_p_d_e:
   1.266 +  assumes "deflation d"
   1.267 +  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   1.268 +  shows "deflation (p oo d oo e)"
   1.269 +proof -
   1.270 +  interpret d: deflation d by fact
   1.271 +  {
   1.272 +    fix x
   1.273 +    have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
   1.274 +      by (rule d.below)
   1.275 +    hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
   1.276 +      by (rule monofun_cfun_arg)
   1.277 +    hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
   1.278 +      by simp
   1.279 +  }
   1.280 +  note p_d_e_below = this
   1.281 +  show ?thesis
   1.282 +  proof
   1.283 +    fix x
   1.284 +    show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
   1.285 +      by (rule p_d_e_below)
   1.286 +  next
   1.287 +    fix x
   1.288 +    show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
   1.289 +    proof (rule below_antisym)
   1.290 +      show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
   1.291 +        by (rule p_d_e_below)
   1.292 +      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)))))"
   1.293 +        by (intro monofun_cfun_arg d)
   1.294 +      hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
   1.295 +        by (simp only: d.idem)
   1.296 +      thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
   1.297 +        by simp
   1.298 +    qed
   1.299 +  qed
   1.300 +qed
   1.301 +
   1.302 +lemma finite_deflation_p_d_e:
   1.303 +  assumes "finite_deflation d"
   1.304 +  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   1.305 +  shows "finite_deflation (p oo d oo e)"
   1.306 +proof -
   1.307 +  interpret d: finite_deflation d by fact
   1.308 +  show ?thesis
   1.309 +  proof (rule finite_deflation_intro)
   1.310 +    have "deflation d" ..
   1.311 +    thus "deflation (p oo d oo e)"
   1.312 +      using d by (rule deflation_p_d_e)
   1.313 +  next
   1.314 +    have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
   1.315 +      by (rule d.finite_image)
   1.316 +    hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
   1.317 +      by (rule finite_imageI)
   1.318 +    hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
   1.319 +      by (simp add: image_image)
   1.320 +    thus "finite {x. (p oo d oo e)\<cdot>x = x}"
   1.321 +      by (rule finite_range_imp_finite_fixes)
   1.322 +  qed
   1.323 +qed
   1.324 +
   1.325 +end
   1.326 +
   1.327 +subsection {* Uniqueness of ep-pairs *}
   1.328 +
   1.329 +lemma ep_pair_unique_e_lemma:
   1.330 +  assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
   1.331 +  shows "e1 \<sqsubseteq> e2"
   1.332 +proof (rule cfun_belowI)
   1.333 +  fix x
   1.334 +  have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
   1.335 +    by (rule ep_pair.e_p_below [OF 1])
   1.336 +  thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
   1.337 +    by (simp only: ep_pair.e_inverse [OF 2])
   1.338 +qed
   1.339 +
   1.340 +lemma ep_pair_unique_e:
   1.341 +  "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
   1.342 +by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
   1.343 +
   1.344 +lemma ep_pair_unique_p_lemma:
   1.345 +  assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
   1.346 +  shows "p1 \<sqsubseteq> p2"
   1.347 +proof (rule cfun_belowI)
   1.348 +  fix x
   1.349 +  have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
   1.350 +    by (rule ep_pair.e_p_below [OF 1])
   1.351 +  hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
   1.352 +    by (rule monofun_cfun_arg)
   1.353 +  thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
   1.354 +    by (simp only: ep_pair.e_inverse [OF 2])
   1.355 +qed
   1.356 +
   1.357 +lemma ep_pair_unique_p:
   1.358 +  "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
   1.359 +by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
   1.360 +
   1.361 +subsection {* Composing ep-pairs *}
   1.362 +
   1.363 +lemma ep_pair_ID_ID: "ep_pair ID ID"
   1.364 +by default simp_all
   1.365 +
   1.366 +lemma ep_pair_comp:
   1.367 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
   1.368 +  shows "ep_pair (e2 oo e1) (p1 oo p2)"
   1.369 +proof
   1.370 +  interpret ep1: ep_pair e1 p1 by fact
   1.371 +  interpret ep2: ep_pair e2 p2 by fact
   1.372 +  fix x y
   1.373 +  show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
   1.374 +    by simp
   1.375 +  have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
   1.376 +    by (rule ep1.e_p_below)
   1.377 +  hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
   1.378 +    by (rule monofun_cfun_arg)
   1.379 +  also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
   1.380 +    by (rule ep2.e_p_below)
   1.381 +  finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
   1.382 +    by simp
   1.383 +qed
   1.384 +
   1.385 +locale pcpo_ep_pair = ep_pair +
   1.386 +  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
   1.387 +  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
   1.388 +begin
   1.389 +
   1.390 +lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
   1.391 +proof -
   1.392 +  have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
   1.393 +  hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
   1.394 +  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
   1.395 +  finally show "e\<cdot>\<bottom> = \<bottom>" by simp
   1.396 +qed
   1.397 +
   1.398 +lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
   1.399 +by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
   1.400 +
   1.401 +lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
   1.402 +by simp
   1.403 +
   1.404 +lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
   1.405 +by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
   1.406 +
   1.407 +lemmas stricts = e_strict p_strict
   1.408 +
   1.409 +end
   1.410 +
   1.411 +end