new theory of powerdomains
authorhuffman
Mon Jan 14 19:26:41 2008 +0100 (2008-01-14)
changeset 259048161f137b0e9
parent 25903 5e59af604d4f
child 25905 098469c6c351
new theory of powerdomains
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/HOLCF.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Mon Jan 14 19:26:41 2008 +0100
     1.3 @@ -0,0 +1,686 @@
     1.4 +(*  Title:      HOLCF/CompactBasis.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Brian Huffman
     1.7 +*)
     1.8 +
     1.9 +header {* Compact bases of domains *}
    1.10 +
    1.11 +theory CompactBasis
    1.12 +imports Bifinite SetPcpo
    1.13 +begin
    1.14 +
    1.15 +subsection {* Ideals over a preorder *}
    1.16 +
    1.17 +locale preorder =
    1.18 +  fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool"
    1.19 +  assumes refl: "r x x"
    1.20 +  assumes trans: "\<lbrakk>r x y; r y z\<rbrakk> \<Longrightarrow> r x z"
    1.21 +begin
    1.22 +
    1.23 +definition
    1.24 +  ideal :: "'a set \<Rightarrow> bool" where
    1.25 +  "ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. r x z \<and> r y z) \<and>
    1.26 +    (\<forall>x y. r x y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
    1.27 +
    1.28 +lemma idealI:
    1.29 +  assumes "\<exists>x. x \<in> A"
    1.30 +  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. r x z \<and> r y z"
    1.31 +  assumes "\<And>x y. \<lbrakk>r x y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
    1.32 +  shows "ideal A"
    1.33 +unfolding ideal_def using prems by fast
    1.34 +
    1.35 +lemma idealD1:
    1.36 +  "ideal A \<Longrightarrow> \<exists>x. x \<in> A"
    1.37 +unfolding ideal_def by fast
    1.38 +
    1.39 +lemma idealD2:
    1.40 +  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. r x z \<and> r y z"
    1.41 +unfolding ideal_def by fast
    1.42 +
    1.43 +lemma idealD3:
    1.44 +  "\<lbrakk>ideal A; r x y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
    1.45 +unfolding ideal_def by fast
    1.46 +
    1.47 +lemma ideal_directed_finite:
    1.48 +  assumes A: "ideal A"
    1.49 +  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. r x z"
    1.50 +apply (induct U set: finite)
    1.51 +apply (simp add: idealD1 [OF A])
    1.52 +apply (simp, clarify, rename_tac y)
    1.53 +apply (drule (1) idealD2 [OF A])
    1.54 +apply (clarify, erule_tac x=z in rev_bexI)
    1.55 +apply (fast intro: trans)
    1.56 +done
    1.57 +
    1.58 +lemma ideal_principal: "ideal {x. r x z}"
    1.59 +apply (rule idealI)
    1.60 +apply (rule_tac x=z in exI)
    1.61 +apply (fast intro: refl)
    1.62 +apply (rule_tac x=z in bexI, fast)
    1.63 +apply (fast intro: refl)
    1.64 +apply (fast intro: trans)
    1.65 +done
    1.66 +
    1.67 +lemma directed_image_ideal:
    1.68 +  assumes A: "ideal A"
    1.69 +  assumes f: "\<And>x y. r x y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.70 +  shows "directed (f ` A)"
    1.71 +apply (rule directedI)
    1.72 +apply (cut_tac idealD1 [OF A], fast)
    1.73 +apply (clarify, rename_tac a b)
    1.74 +apply (drule (1) idealD2 [OF A])
    1.75 +apply (clarify, rename_tac c)
    1.76 +apply (rule_tac x="f c" in rev_bexI)
    1.77 +apply (erule imageI)
    1.78 +apply (simp add: f)
    1.79 +done
    1.80 +
    1.81 +lemma adm_ideal: "adm (\<lambda>A. ideal A)"
    1.82 +unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
    1.83 +
    1.84 +end
    1.85 +
    1.86 +subsection {* Defining functions in terms of basis elements *}
    1.87 +
    1.88 +lemma (in preorder) lub_image_principal:
    1.89 +  assumes f: "\<And>x y. r x y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.90 +  shows "(\<Squnion>x\<in>{x. r x y}. f x) = f y"
    1.91 +apply (rule thelubI)
    1.92 +apply (rule is_lub_maximal)
    1.93 +apply (rule ub_imageI)
    1.94 +apply (simp add: f)
    1.95 +apply (rule imageI)
    1.96 +apply (simp add: refl)
    1.97 +done
    1.98 +
    1.99 +lemma finite_directed_has_lub: "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u. S <<| u"
   1.100 +apply (drule (1) directed_finiteD, rule subset_refl)
   1.101 +apply (erule bexE)
   1.102 +apply (rule_tac x=z in exI)
   1.103 +apply (erule (1) is_lub_maximal)
   1.104 +done
   1.105 +
   1.106 +lemma is_ub_thelub0: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
   1.107 +apply (erule exE, drule lubI)
   1.108 +apply (drule is_lubD1)
   1.109 +apply (erule (1) is_ubD)
   1.110 +done
   1.111 +
   1.112 +lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
   1.113 +by (erule exE, drule lubI, erule is_lub_lub)
   1.114 +
   1.115 +locale bifinite_basis = preorder +
   1.116 +  fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   1.117 +  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
   1.118 +  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
   1.119 +  assumes cont_approxes: "cont approxes"
   1.120 +  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
   1.121 +  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
   1.122 +
   1.123 +  fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
   1.124 +  assumes take_less: "r (take n a) a"
   1.125 +  assumes take_take: "take n (take n a) = take n a"
   1.126 +  assumes take_mono: "r a b \<Longrightarrow> r (take n a) (take n b)"
   1.127 +  assumes take_chain: "r (take n a) (take (Suc n) a)"
   1.128 +  assumes finite_range_take: "finite (range (take n))"
   1.129 +  assumes take_covers: "\<exists>n. take n a = a"
   1.130 +begin
   1.131 +
   1.132 +lemma finite_take_approxes: "finite (take n ` approxes x)"
   1.133 +by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take])
   1.134 +
   1.135 +lemma basis_fun_lemma0:
   1.136 +  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.137 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.138 +  shows "\<exists>u. f ` take i ` approxes x <<| u"
   1.139 +apply (rule finite_directed_has_lub)
   1.140 +apply (rule finite_imageI)
   1.141 +apply (rule finite_take_approxes)
   1.142 +apply (subst image_image)
   1.143 +apply (rule directed_image_ideal)
   1.144 +apply (rule ideal_approxes)
   1.145 +apply (rule f_mono)
   1.146 +apply (erule take_mono)
   1.147 +done
   1.148 +
   1.149 +lemma basis_fun_lemma1:
   1.150 +  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.151 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.152 +  shows "chain (\<lambda>i. lub (f ` take i ` approxes x))"
   1.153 + apply (rule chainI)
   1.154 + apply (rule is_lub_thelub0)
   1.155 +  apply (rule basis_fun_lemma0, erule f_mono)
   1.156 + apply (rule is_ubI, clarsimp, rename_tac a)
   1.157 + apply (rule trans_less [OF f_mono [OF take_chain]])
   1.158 + apply (rule is_ub_thelub0)
   1.159 +  apply (rule basis_fun_lemma0, erule f_mono)
   1.160 + apply simp
   1.161 +done
   1.162 +
   1.163 +lemma basis_fun_lemma2:
   1.164 +  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.165 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.166 +  shows "f ` approxes x <<| (\<Squnion>i. lub (f ` take i ` approxes x))"
   1.167 + apply (rule is_lubI)
   1.168 + apply (rule ub_imageI, rename_tac a)
   1.169 +  apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
   1.170 +  apply (erule subst)
   1.171 +  apply (rule rev_trans_less)
   1.172 +   apply (rule_tac x=i in is_ub_thelub)
   1.173 +   apply (rule basis_fun_lemma1, erule f_mono)
   1.174 +  apply (rule is_ub_thelub0)
   1.175 +   apply (rule basis_fun_lemma0, erule f_mono)
   1.176 +  apply simp
   1.177 + apply (rule is_lub_thelub [OF _ ub_rangeI])
   1.178 +  apply (rule basis_fun_lemma1, erule f_mono)
   1.179 + apply (rule is_lub_thelub0)
   1.180 +  apply (rule basis_fun_lemma0, erule f_mono)
   1.181 + apply (rule is_ubI, clarsimp, rename_tac a)
   1.182 + apply (rule trans_less [OF f_mono [OF take_less]])
   1.183 + apply (erule (1) ub_imageD)
   1.184 +done
   1.185 +
   1.186 +lemma basis_fun_lemma:
   1.187 +  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.188 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.189 +  shows "\<exists>u. f ` approxes x <<| u"
   1.190 +by (rule exI, rule basis_fun_lemma2, erule f_mono)
   1.191 +
   1.192 +lemma approxes_mono: "x \<sqsubseteq> y \<Longrightarrow> approxes x \<subseteq> approxes y"
   1.193 +apply (drule cont_approxes [THEN cont2mono, THEN monofunE])
   1.194 +apply (simp add: set_cpo_simps)
   1.195 +done
   1.196 +
   1.197 +lemma approxes_contlub:
   1.198 +  "chain Y \<Longrightarrow> approxes (\<Squnion>i. Y i) = (\<Union>i. approxes (Y i))"
   1.199 +by (simp add: cont2contlubE [OF cont_approxes] set_cpo_simps)
   1.200 +
   1.201 +lemma less_def: "(x \<sqsubseteq> y) = (approxes x \<subseteq> approxes y)"
   1.202 +by (rule iffI [OF approxes_mono subset_approxesD])
   1.203 +
   1.204 +lemma approxes_eq: "approxes x = {a. principal a \<sqsubseteq> x}"
   1.205 +unfolding less_def approxes_principal
   1.206 +apply safe
   1.207 +apply (erule (1) idealD3 [OF ideal_approxes])
   1.208 +apply (erule subsetD, simp add: refl)
   1.209 +done
   1.210 +
   1.211 +lemma mem_approxes_iff: "(a \<in> approxes x) = (principal a \<sqsubseteq> x)"
   1.212 +by (simp add: approxes_eq)
   1.213 +
   1.214 +lemma principal_less_iff: "(principal a \<sqsubseteq> x) = (a \<in> approxes x)"
   1.215 +by (simp add: approxes_eq)
   1.216 +
   1.217 +lemma approxesD: "a \<in> approxes x \<Longrightarrow> principal a \<sqsubseteq> x"
   1.218 +by (simp add: approxes_eq)
   1.219 +
   1.220 +lemma principal_mono: "r a b \<Longrightarrow> principal a \<sqsubseteq> principal b"
   1.221 +by (rule approxesD, simp add: approxes_principal)
   1.222 +
   1.223 +lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
   1.224 +unfolding principal_less_iff
   1.225 +by (simp add: less_def subset_def)
   1.226 +
   1.227 +lemma lub_principal_approxes: "principal ` approxes x <<| x"
   1.228 +apply (rule is_lubI)
   1.229 +apply (rule ub_imageI)
   1.230 +apply (erule approxesD)
   1.231 +apply (subst less_def)
   1.232 +apply (rule subsetI)
   1.233 +apply (drule (1) ub_imageD)
   1.234 +apply (simp add: approxes_eq)
   1.235 +done
   1.236 +
   1.237 +definition
   1.238 +  basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
   1.239 +  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` approxes x)))"
   1.240 +
   1.241 +lemma basis_fun_beta:
   1.242 +  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.243 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.244 +  shows "basis_fun f\<cdot>x = lub (f ` approxes x)"
   1.245 +unfolding basis_fun_def
   1.246 +proof (rule beta_cfun)
   1.247 +  have lub: "\<And>x. \<exists>u. f ` approxes x <<| u"
   1.248 +    using f_mono by (rule basis_fun_lemma)
   1.249 +  show cont: "cont (\<lambda>x. lub (f ` approxes x))"
   1.250 +    apply (rule contI2)
   1.251 +     apply (rule monofunI)
   1.252 +     apply (rule is_lub_thelub0 [OF lub ub_imageI])
   1.253 +     apply (rule is_ub_thelub0 [OF lub imageI])
   1.254 +     apply (erule (1) subsetD [OF approxes_mono])
   1.255 +    apply (rule is_lub_thelub0 [OF lub ub_imageI])
   1.256 +    apply (simp add: approxes_contlub, clarify)
   1.257 +    apply (erule rev_trans_less [OF is_ub_thelub])
   1.258 +    apply (erule is_ub_thelub0 [OF lub imageI])
   1.259 +    done
   1.260 +qed
   1.261 +
   1.262 +lemma basis_fun_principal:
   1.263 +  fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.264 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.265 +  shows "basis_fun f\<cdot>(principal a) = f a"
   1.266 +apply (subst basis_fun_beta, erule f_mono)
   1.267 +apply (subst approxes_principal)
   1.268 +apply (rule lub_image_principal, erule f_mono)
   1.269 +done
   1.270 +
   1.271 +lemma basis_fun_mono:
   1.272 +  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.273 +  assumes g_mono: "\<And>a b. r a b \<Longrightarrow> g a \<sqsubseteq> g b"
   1.274 +  assumes less: "\<And>a. f a \<sqsubseteq> g a"
   1.275 +  shows "basis_fun f \<sqsubseteq> basis_fun g"
   1.276 + apply (rule less_cfun_ext)
   1.277 + apply (simp only: basis_fun_beta f_mono g_mono)
   1.278 + apply (rule is_lub_thelub0)
   1.279 +  apply (rule basis_fun_lemma, erule f_mono)
   1.280 + apply (rule ub_imageI, rename_tac a)
   1.281 + apply (rule trans_less [OF less])
   1.282 + apply (rule is_ub_thelub0)
   1.283 +  apply (rule basis_fun_lemma, erule g_mono)
   1.284 + apply (erule imageI)
   1.285 +done
   1.286 +
   1.287 +lemma compact_principal: "compact (principal a)"
   1.288 +by (rule compactI2, simp add: principal_less_iff approxes_contlub)
   1.289 +
   1.290 +lemma chain_basis_fun_take:
   1.291 +  "chain (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
   1.292 +apply (rule chainI)
   1.293 +apply (rule basis_fun_mono)
   1.294 +apply (erule principal_mono [OF take_mono])
   1.295 +apply (erule principal_mono [OF take_mono])
   1.296 +apply (rule principal_mono [OF take_chain])
   1.297 +done
   1.298 +
   1.299 +lemma lub_basis_fun_take:
   1.300 +  "(\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x) = x"
   1.301 + apply (simp add: basis_fun_beta principal_mono take_mono)
   1.302 + apply (subst image_image [where f=principal, symmetric])
   1.303 + apply (rule unique_lub [OF _ lub_principal_approxes])
   1.304 + apply (rule basis_fun_lemma2, erule principal_mono)
   1.305 +done
   1.306 +
   1.307 +lemma finite_directed_contains_lub:
   1.308 +  "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> \<exists>u\<in>S. S <<| u"
   1.309 +apply (drule (1) directed_finiteD, rule subset_refl)
   1.310 +apply (erule bexE)
   1.311 +apply (rule rev_bexI, assumption)
   1.312 +apply (erule (1) is_lub_maximal)
   1.313 +done
   1.314 +
   1.315 +lemma lub_finite_directed_in_self:
   1.316 +  "\<lbrakk>finite S; directed S\<rbrakk> \<Longrightarrow> lub S \<in> S"
   1.317 +apply (drule (1) directed_finiteD, rule subset_refl)
   1.318 +apply (erule bexE)
   1.319 +apply (drule (1) is_lub_maximal)
   1.320 +apply (drule thelubI)
   1.321 +apply simp
   1.322 +done
   1.323 +
   1.324 +lemma basis_fun_take_eq_principal:
   1.325 +  "\<exists>a\<in>approxes x.
   1.326 +    basis_fun (\<lambda>a. principal (take i a))\<cdot>x = principal (take i a)"
   1.327 + apply (simp add: basis_fun_beta principal_mono take_mono)
   1.328 + apply (subst image_image [where f=principal, symmetric])
   1.329 + apply (subgoal_tac "finite (principal ` take i ` approxes x)")
   1.330 +  apply (subgoal_tac "directed (principal ` take i ` approxes x)")
   1.331 +   apply (drule (1) lub_finite_directed_in_self, fast)
   1.332 +  apply (subst image_image)
   1.333 +  apply (rule directed_image_ideal)
   1.334 +   apply (rule ideal_approxes)
   1.335 +  apply (erule principal_mono [OF take_mono])
   1.336 + apply (rule finite_imageI)
   1.337 + apply (rule finite_take_approxes)
   1.338 +done
   1.339 +
   1.340 +lemma principal_induct:
   1.341 +  assumes adm: "adm P"
   1.342 +  assumes P: "\<And>a. P (principal a)"
   1.343 +  shows "P x"
   1.344 + apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
   1.345 + apply (simp add: lub_basis_fun_take)
   1.346 + apply (rule admD [rule_format, OF adm])
   1.347 +  apply (simp add: chain_basis_fun_take)
   1.348 + apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
   1.349 + apply (clarify, simp add: P)
   1.350 +done
   1.351 +
   1.352 +lemma finite_fixes_basis_fun_take:
   1.353 +  "finite {x. basis_fun (\<lambda>a. principal (take i a))\<cdot>x = x}" (is "finite ?S")
   1.354 +apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
   1.355 +apply (erule finite_subset)
   1.356 +apply (rule finite_imageI)
   1.357 +apply (rule finite_range_take)
   1.358 +apply (clarify, erule subst)
   1.359 +apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
   1.360 +apply fast
   1.361 +done
   1.362 +
   1.363 +end
   1.364 +
   1.365 +
   1.366 +subsection {* Compact bases of bifinite domains *}
   1.367 +
   1.368 +defaultsort bifinite
   1.369 +
   1.370 +typedef (open) 'a compact_basis = "{x::'a::bifinite. compact x}"
   1.371 +by (fast intro: compact_approx)
   1.372 +
   1.373 +lemma compact_Rep_compact_basis [simp]: "compact (Rep_compact_basis a)"
   1.374 +by (rule Rep_compact_basis [simplified])
   1.375 +
   1.376 +lemma Rep_Abs_compact_basis_approx [simp]:
   1.377 +  "Rep_compact_basis (Abs_compact_basis (approx n\<cdot>x)) = approx n\<cdot>x"
   1.378 +by (rule Abs_compact_basis_inverse, simp)
   1.379 +
   1.380 +lemma compact_imp_Rep_compact_basis:
   1.381 +  "compact x \<Longrightarrow> \<exists>y. x = Rep_compact_basis y"
   1.382 +by (rule exI, rule Abs_compact_basis_inverse [symmetric], simp)
   1.383 +
   1.384 +definition
   1.385 +  compact_le :: "'a compact_basis \<Rightarrow> 'a compact_basis \<Rightarrow> bool" where
   1.386 +  "compact_le = (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
   1.387 +
   1.388 +lemma compact_le_refl: "compact_le x x"
   1.389 +unfolding compact_le_def by (rule refl_less)
   1.390 +
   1.391 +lemma compact_le_trans: "\<lbrakk>compact_le x y; compact_le y z\<rbrakk> \<Longrightarrow> compact_le x z"
   1.392 +unfolding compact_le_def by (rule trans_less)
   1.393 +
   1.394 +lemma compact_le_antisym: "\<lbrakk>compact_le x y; compact_le y x\<rbrakk> \<Longrightarrow> x = y"
   1.395 +unfolding compact_le_def
   1.396 +apply (rule Rep_compact_basis_inject [THEN iffD1])
   1.397 +apply (erule (1) antisym_less)
   1.398 +done
   1.399 +
   1.400 +interpretation compact_le: preorder [compact_le]
   1.401 +by (rule preorder.intro, rule compact_le_refl, rule compact_le_trans)
   1.402 +
   1.403 +text {* minimal compact element *}
   1.404 +
   1.405 +definition
   1.406 +  compact_bot :: "'a compact_basis" where
   1.407 +  "compact_bot = Abs_compact_basis \<bottom>"
   1.408 +
   1.409 +lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
   1.410 +unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
   1.411 +
   1.412 +lemma compact_minimal [simp]: "compact_le compact_bot a"
   1.413 +unfolding compact_le_def Rep_compact_bot by simp
   1.414 +
   1.415 +text {* compacts *}
   1.416 +
   1.417 +definition
   1.418 +  compacts :: "'a \<Rightarrow> 'a compact_basis set" where
   1.419 +  "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
   1.420 +
   1.421 +lemma ideal_compacts: "compact_le.ideal (compacts w)"
   1.422 +unfolding compacts_def
   1.423 + apply (rule compact_le.idealI)
   1.424 +   apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
   1.425 +   apply (simp add: approx_less)
   1.426 +  apply simp
   1.427 +  apply (cut_tac a=x in compact_Rep_compact_basis)
   1.428 +  apply (cut_tac a=y in compact_Rep_compact_basis)
   1.429 +  apply (drule bifinite_compact_eq_approx)
   1.430 +  apply (drule bifinite_compact_eq_approx)
   1.431 +  apply (clarify, rename_tac i j)
   1.432 +  apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
   1.433 +  apply (simp add: approx_less compact_le_def)
   1.434 +  apply (erule subst, erule subst)
   1.435 +  apply (simp add: monofun_cfun chain_mono3 [OF chain_approx])
   1.436 + apply (simp add: compact_le_def)
   1.437 + apply (erule (1) trans_less)
   1.438 +done
   1.439 +
   1.440 +lemma compacts_Rep_compact_basis:
   1.441 +  "compacts (Rep_compact_basis b) = {a. compact_le a b}"
   1.442 +unfolding compacts_def compact_le_def ..
   1.443 +
   1.444 +lemma cont_compacts: "cont compacts"
   1.445 +unfolding compacts_def
   1.446 +apply (rule contI2)
   1.447 +apply (rule monofunI)
   1.448 +apply (simp add: set_cpo_simps)
   1.449 +apply (fast intro: trans_less)
   1.450 +apply (simp add: set_cpo_simps)
   1.451 +apply clarify
   1.452 +apply simp
   1.453 +apply (erule (1) compactD2 [OF compact_Rep_compact_basis])
   1.454 +done
   1.455 +
   1.456 +lemma compacts_lessD: "compacts x \<subseteq> compacts y \<Longrightarrow> x \<sqsubseteq> y"
   1.457 +apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
   1.458 +apply (rule admD [rule_format], simp, simp)
   1.459 +apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
   1.460 +apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
   1.461 +apply (simp add: compacts_def Abs_compact_basis_inverse)
   1.462 +done
   1.463 +
   1.464 +lemma compacts_mono: "x \<sqsubseteq> y \<Longrightarrow> compacts x \<subseteq> compacts y"
   1.465 +unfolding compacts_def by (fast intro: trans_less)
   1.466 +
   1.467 +lemma less_compact_basis_iff: "(x \<sqsubseteq> y) = (compacts x \<subseteq> compacts y)"
   1.468 +by (rule iffI [OF compacts_mono compacts_lessD])
   1.469 +
   1.470 +lemma compact_basis_induct:
   1.471 +  "\<lbrakk>adm P; \<And>a. P (Rep_compact_basis a)\<rbrakk> \<Longrightarrow> P x"
   1.472 +apply (erule approx_induct)
   1.473 +apply (drule_tac x="Abs_compact_basis (approx n\<cdot>x)" in meta_spec)
   1.474 +apply (simp add: Abs_compact_basis_inverse)
   1.475 +done
   1.476 +
   1.477 +text {* approximation on compact bases *}
   1.478 +
   1.479 +definition
   1.480 +  compact_approx :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
   1.481 +  "compact_approx = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
   1.482 +
   1.483 +lemma Rep_compact_approx:
   1.484 +  "Rep_compact_basis (compact_approx n a) = approx n\<cdot>(Rep_compact_basis a)"
   1.485 +unfolding compact_approx_def
   1.486 +by (simp add: Abs_compact_basis_inverse)
   1.487 +
   1.488 +lemmas approx_Rep_compact_basis = Rep_compact_approx [symmetric]
   1.489 +
   1.490 +lemma compact_approx_le:
   1.491 +  "compact_le (compact_approx n a) a"
   1.492 +unfolding compact_le_def
   1.493 +by (simp add: Rep_compact_approx approx_less)
   1.494 +
   1.495 +lemma compact_approx_mono1:
   1.496 +  "i \<le> j \<Longrightarrow> compact_le (compact_approx i a) (compact_approx j a)"
   1.497 +unfolding compact_le_def
   1.498 +apply (simp add: Rep_compact_approx)
   1.499 +apply (rule chain_mono3, simp, assumption)
   1.500 +done
   1.501 +
   1.502 +lemma compact_approx_mono:
   1.503 +  "compact_le a b \<Longrightarrow> compact_le (compact_approx n a) (compact_approx n b)"
   1.504 +unfolding compact_le_def
   1.505 +apply (simp add: Rep_compact_approx)
   1.506 +apply (erule monofun_cfun_arg)
   1.507 +done
   1.508 +
   1.509 +lemma ex_compact_approx_eq: "\<exists>n. compact_approx n a = a"
   1.510 +apply (simp add: Rep_compact_basis_inject [symmetric])
   1.511 +apply (simp add: Rep_compact_approx)
   1.512 +apply (rule bifinite_compact_eq_approx)
   1.513 +apply (rule compact_Rep_compact_basis)
   1.514 +done
   1.515 +
   1.516 +lemma compact_approx_idem:
   1.517 +  "compact_approx n (compact_approx n a) = compact_approx n a"
   1.518 +apply (rule Rep_compact_basis_inject [THEN iffD1])
   1.519 +apply (simp add: Rep_compact_approx)
   1.520 +done
   1.521 +
   1.522 +lemma finite_fixes_compact_approx: "finite {a. compact_approx n a = a}"
   1.523 +apply (subgoal_tac "finite (Rep_compact_basis ` {a. compact_approx n a = a})")
   1.524 +apply (erule finite_imageD)
   1.525 +apply (rule inj_onI, simp add: Rep_compact_basis_inject)
   1.526 +apply (rule finite_subset [OF _ finite_fixes_approx [where i=n]])
   1.527 +apply (rule subsetI, clarify, rename_tac a)
   1.528 +apply (simp add: Rep_compact_basis_inject [symmetric])
   1.529 +apply (simp add: Rep_compact_approx)
   1.530 +done
   1.531 +
   1.532 +lemma finite_range_compact_approx: "finite (range (compact_approx n))"
   1.533 +apply (cut_tac n=n in finite_fixes_compact_approx)
   1.534 +apply (simp add: idem_fixes_eq_range compact_approx_idem)
   1.535 +apply (simp add: image_def)
   1.536 +done
   1.537 +
   1.538 +interpretation compact_basis:
   1.539 +  bifinite_basis [compact_le Rep_compact_basis compacts compact_approx]
   1.540 +apply unfold_locales
   1.541 +apply (rule ideal_compacts)
   1.542 +apply (rule cont_compacts)
   1.543 +apply (rule compacts_Rep_compact_basis)
   1.544 +apply (erule compacts_lessD)
   1.545 +apply (rule compact_approx_le)
   1.546 +apply (rule compact_approx_idem)
   1.547 +apply (erule compact_approx_mono)
   1.548 +apply (rule compact_approx_mono1, simp)
   1.549 +apply (rule finite_range_compact_approx)
   1.550 +apply (rule ex_compact_approx_eq)
   1.551 +done
   1.552 +
   1.553 +
   1.554 +subsection {* A compact basis for powerdomains *}
   1.555 +
   1.556 +typedef 'a pd_basis =
   1.557 +  "{S::'a::bifinite compact_basis set. finite S \<and> S \<noteq> {}}"
   1.558 +by (rule_tac x="{arbitrary}" in exI, simp)
   1.559 +
   1.560 +lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
   1.561 +by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
   1.562 +
   1.563 +lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
   1.564 +by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
   1.565 +
   1.566 +text {* unit and plus *}
   1.567 +
   1.568 +definition
   1.569 +  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
   1.570 +  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
   1.571 +
   1.572 +definition
   1.573 +  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
   1.574 +  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
   1.575 +
   1.576 +lemma Rep_PDUnit:
   1.577 +  "Rep_pd_basis (PDUnit x) = {x}"
   1.578 +unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
   1.579 +
   1.580 +lemma Rep_PDPlus:
   1.581 +  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
   1.582 +unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
   1.583 +
   1.584 +lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
   1.585 +unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
   1.586 +
   1.587 +lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
   1.588 +unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
   1.589 +
   1.590 +lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
   1.591 +unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
   1.592 +
   1.593 +lemma PDPlus_absorb: "PDPlus t t = t"
   1.594 +unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
   1.595 +
   1.596 +lemma pd_basis_induct1:
   1.597 +  assumes PDUnit: "\<And>a. P (PDUnit a)"
   1.598 +  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
   1.599 +  shows "P x"
   1.600 +apply (induct x, unfold pd_basis_def, clarify)
   1.601 +apply (erule (1) finite_ne_induct)
   1.602 +apply (cut_tac a=x in PDUnit)
   1.603 +apply (simp add: PDUnit_def)
   1.604 +apply (drule_tac a=x in PDPlus)
   1.605 +apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
   1.606 +done
   1.607 +
   1.608 +lemma pd_basis_induct:
   1.609 +  assumes PDUnit: "\<And>a. P (PDUnit a)"
   1.610 +  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
   1.611 +  shows "P x"
   1.612 +apply (induct x rule: pd_basis_induct1)
   1.613 +apply (rule PDUnit, erule PDPlus [OF PDUnit])
   1.614 +done
   1.615 +
   1.616 +text {* fold-pd *}
   1.617 +
   1.618 +definition
   1.619 +  fold_pd ::
   1.620 +    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   1.621 +  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
   1.622 +
   1.623 +lemma (in ACIf) fold_pd_PDUnit:
   1.624 +  "fold_pd g f (PDUnit x) = g x"
   1.625 +unfolding fold_pd_def Rep_PDUnit by simp
   1.626 +
   1.627 +lemma (in ACIf) fold_pd_PDPlus:
   1.628 +  "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   1.629 +unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
   1.630 +
   1.631 +text {* approx-pd *}
   1.632 +
   1.633 +definition
   1.634 +  approx_pd :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
   1.635 +  "approx_pd n = (\<lambda>t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))"
   1.636 +
   1.637 +lemma Rep_approx_pd:
   1.638 +  "Rep_pd_basis (approx_pd n t) = compact_approx n ` Rep_pd_basis t"
   1.639 +unfolding approx_pd_def
   1.640 +apply (rule Abs_pd_basis_inverse)
   1.641 +apply (simp add: pd_basis_def)
   1.642 +done
   1.643 +
   1.644 +lemma approx_pd_simps [simp]:
   1.645 +  "approx_pd n (PDUnit a) = PDUnit (compact_approx n a)"
   1.646 +  "approx_pd n (PDPlus t u) = PDPlus (approx_pd n t) (approx_pd n u)"
   1.647 +apply (simp_all add: Rep_pd_basis_inject [symmetric])
   1.648 +apply (simp_all add: Rep_approx_pd Rep_PDUnit Rep_PDPlus image_Un)
   1.649 +done
   1.650 +
   1.651 +lemma approx_pd_idem: "approx_pd n (approx_pd n t) = approx_pd n t"
   1.652 +apply (induct t rule: pd_basis_induct)
   1.653 +apply (simp add: compact_approx_idem)
   1.654 +apply simp
   1.655 +done
   1.656 +
   1.657 +lemma range_image_f: "range (image f) = Pow (range f)"
   1.658 +apply (safe, fast)
   1.659 +apply (rule_tac x="f -` x" in range_eqI)
   1.660 +apply (simp, fast)
   1.661 +done
   1.662 +
   1.663 +lemma finite_range_approx_pd: "finite (range (approx_pd n))"
   1.664 +apply (subgoal_tac "finite (Rep_pd_basis ` range (approx_pd n))")
   1.665 +apply (erule finite_imageD)
   1.666 +apply (rule inj_onI, simp add: Rep_pd_basis_inject)
   1.667 +apply (subst image_image)
   1.668 +apply (subst Rep_approx_pd)
   1.669 +apply (simp only: range_composition)
   1.670 +apply (rule finite_subset [OF image_mono [OF subset_UNIV]])
   1.671 +apply (simp add: range_image_f)
   1.672 +apply (rule finite_range_compact_approx)
   1.673 +done
   1.674 +
   1.675 +lemma ex_approx_pd_eq: "\<exists>n. approx_pd n t = t"
   1.676 +apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. approx_pd m t = t", fast)
   1.677 +apply (induct t rule: pd_basis_induct)
   1.678 +apply (cut_tac a=a in ex_compact_approx_eq)
   1.679 +apply (clarify, rule_tac x=n in exI)
   1.680 +apply (clarify, simp)
   1.681 +apply (rule compact_le_antisym)
   1.682 +apply (rule compact_approx_le)
   1.683 +apply (drule_tac a=a in compact_approx_mono1)
   1.684 +apply simp
   1.685 +apply (clarify, rename_tac i j)
   1.686 +apply (rule_tac x="max i j" in exI, simp)
   1.687 +done
   1.688 +
   1.689 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Mon Jan 14 19:26:41 2008 +0100
     2.3 @@ -0,0 +1,630 @@
     2.4 +(*  Title:      HOLCF/ConvexPD.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Brian Huffman
     2.7 +*)
     2.8 +
     2.9 +header {* Convex powerdomain *}
    2.10 +
    2.11 +theory ConvexPD
    2.12 +imports UpperPD LowerPD
    2.13 +begin
    2.14 +
    2.15 +subsection {* Basis preorder *}
    2.16 +
    2.17 +definition
    2.18 +  convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<natural>" 50) where
    2.19 +  "convex_le = (\<lambda>u v. u \<le>\<sharp> v \<and> u \<le>\<flat> v)"
    2.20 +
    2.21 +lemma convex_le_refl [simp]: "t \<le>\<natural> t"
    2.22 +unfolding convex_le_def by (fast intro: upper_le_refl lower_le_refl)
    2.23 +
    2.24 +lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
    2.25 +unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
    2.26 +
    2.27 +interpretation convex_le: preorder [convex_le]
    2.28 +by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
    2.29 +
    2.30 +lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
    2.31 +unfolding convex_le_def Rep_PDUnit by simp
    2.32 +
    2.33 +lemma PDUnit_convex_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
    2.34 +unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono)
    2.35 +
    2.36 +lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v"
    2.37 +unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
    2.38 +
    2.39 +lemma convex_le_PDUnit_PDUnit_iff [simp]:
    2.40 +  "(PDUnit a \<le>\<natural> PDUnit b) = compact_le a b"
    2.41 +unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
    2.42 +
    2.43 +lemma convex_le_PDUnit_lemma1:
    2.44 +  "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. compact_le a b)"
    2.45 +unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
    2.46 +using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
    2.47 +
    2.48 +lemma convex_le_PDUnit_PDPlus_iff [simp]:
    2.49 +  "(PDUnit a \<le>\<natural> PDPlus t u) = (PDUnit a \<le>\<natural> t \<and> PDUnit a \<le>\<natural> u)"
    2.50 +unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast
    2.51 +
    2.52 +lemma convex_le_PDUnit_lemma2:
    2.53 +  "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. compact_le a b)"
    2.54 +unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
    2.55 +using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
    2.56 +
    2.57 +lemma convex_le_PDPlus_PDUnit_iff [simp]:
    2.58 +  "(PDPlus t u \<le>\<natural> PDUnit a) = (t \<le>\<natural> PDUnit a \<and> u \<le>\<natural> PDUnit a)"
    2.59 +unfolding convex_le_PDUnit_lemma2 Rep_PDPlus by fast
    2.60 +
    2.61 +lemma convex_le_PDPlus_lemma:
    2.62 +  assumes z: "PDPlus t u \<le>\<natural> z"
    2.63 +  shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w"
    2.64 +proof (intro exI conjI)
    2.65 +  let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. compact_le a b}"
    2.66 +  let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. compact_le a b}"
    2.67 +  let ?v = "Abs_pd_basis ?A"
    2.68 +  let ?w = "Abs_pd_basis ?B"
    2.69 +  have Rep_v: "Rep_pd_basis ?v = ?A"
    2.70 +    apply (rule Abs_pd_basis_inverse)
    2.71 +    apply (rule Rep_pd_basis_nonempty [of t, folded ex_in_conv, THEN exE])
    2.72 +    apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify)
    2.73 +    apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE)
    2.74 +    apply (simp add: pd_basis_def)
    2.75 +    apply fast
    2.76 +    done
    2.77 +  have Rep_w: "Rep_pd_basis ?w = ?B"
    2.78 +    apply (rule Abs_pd_basis_inverse)
    2.79 +    apply (rule Rep_pd_basis_nonempty [of u, folded ex_in_conv, THEN exE])
    2.80 +    apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify)
    2.81 +    apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE)
    2.82 +    apply (simp add: pd_basis_def)
    2.83 +    apply fast
    2.84 +    done
    2.85 +  show "z = PDPlus ?v ?w"
    2.86 +    apply (insert z)
    2.87 +    apply (simp add: convex_le_def, erule conjE)
    2.88 +    apply (simp add: Rep_pd_basis_inject [symmetric] Rep_PDPlus)
    2.89 +    apply (simp add: Rep_v Rep_w)
    2.90 +    apply (rule equalityI)
    2.91 +     apply (rule subsetI)
    2.92 +     apply (simp only: upper_le_def)
    2.93 +     apply (drule (1) bspec, erule bexE)
    2.94 +     apply (simp add: Rep_PDPlus)
    2.95 +     apply fast
    2.96 +    apply fast
    2.97 +    done
    2.98 +  show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w"
    2.99 +   apply (insert z)
   2.100 +   apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w)
   2.101 +   apply fast+
   2.102 +   done
   2.103 +qed
   2.104 +
   2.105 +lemma convex_le_induct [induct set: convex_le]:
   2.106 +  assumes le: "t \<le>\<natural> u"
   2.107 +  assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v"
   2.108 +  assumes 3: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
   2.109 +  assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
   2.110 +  shows "P t u"
   2.111 +using le apply (induct t arbitrary: u rule: pd_basis_induct)
   2.112 +apply (erule rev_mp)
   2.113 +apply (induct_tac u rule: pd_basis_induct1)
   2.114 +apply (simp add: 3)
   2.115 +apply (simp, clarify, rename_tac a b t)
   2.116 +apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)")
   2.117 +apply (simp add: PDPlus_absorb)
   2.118 +apply (erule (1) 4 [OF 3])
   2.119 +apply (drule convex_le_PDPlus_lemma, clarify)
   2.120 +apply (simp add: 4)
   2.121 +done
   2.122 +
   2.123 +lemma approx_pd_convex_mono1:
   2.124 +  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<natural> approx_pd j t"
   2.125 +apply (induct t rule: pd_basis_induct)
   2.126 +apply (simp add: compact_approx_mono1)
   2.127 +apply (simp add: PDPlus_convex_mono)
   2.128 +done
   2.129 +
   2.130 +lemma approx_pd_convex_le: "approx_pd i t \<le>\<natural> t"
   2.131 +apply (induct t rule: pd_basis_induct)
   2.132 +apply (simp add: compact_approx_le)
   2.133 +apply (simp add: PDPlus_convex_mono)
   2.134 +done
   2.135 +
   2.136 +lemma approx_pd_convex_mono:
   2.137 +  "t \<le>\<natural> u \<Longrightarrow> approx_pd n t \<le>\<natural> approx_pd n u"
   2.138 +apply (erule convex_le_induct)
   2.139 +apply (erule (1) convex_le_trans)
   2.140 +apply (simp add: compact_approx_mono)
   2.141 +apply (simp add: PDPlus_convex_mono)
   2.142 +done
   2.143 +
   2.144 +
   2.145 +subsection {* Type definition *}
   2.146 +
   2.147 +cpodef (open) 'a convex_pd =
   2.148 +  "{S::'a::bifinite pd_basis set. convex_le.ideal S}"
   2.149 +apply (simp add: convex_le.adm_ideal)
   2.150 +apply (fast intro: convex_le.ideal_principal)
   2.151 +done
   2.152 +
   2.153 +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
   2.154 +by (rule Rep_convex_pd [simplified])
   2.155 +
   2.156 +lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
   2.157 +unfolding less_convex_pd_def less_set_def .
   2.158 +
   2.159 +
   2.160 +subsection {* Principal ideals *}
   2.161 +
   2.162 +definition
   2.163 +  convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
   2.164 +  "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
   2.165 +
   2.166 +lemma Rep_convex_principal:
   2.167 +  "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
   2.168 +unfolding convex_principal_def
   2.169 +apply (rule Abs_convex_pd_inverse [simplified])
   2.170 +apply (rule convex_le.ideal_principal)
   2.171 +done
   2.172 +
   2.173 +interpretation convex_pd:
   2.174 +  bifinite_basis [convex_le convex_principal Rep_convex_pd approx_pd]
   2.175 +apply unfold_locales
   2.176 +apply (rule ideal_Rep_convex_pd)
   2.177 +apply (rule cont_Rep_convex_pd)
   2.178 +apply (rule Rep_convex_principal)
   2.179 +apply (simp only: less_convex_pd_def less_set_def)
   2.180 +apply (rule approx_pd_convex_le)
   2.181 +apply (rule approx_pd_idem)
   2.182 +apply (erule approx_pd_convex_mono)
   2.183 +apply (rule approx_pd_convex_mono1, simp)
   2.184 +apply (rule finite_range_approx_pd)
   2.185 +apply (rule ex_approx_pd_eq)
   2.186 +done
   2.187 +
   2.188 +lemma convex_principal_less_iff [simp]:
   2.189 +  "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
   2.190 +unfolding less_convex_pd_def Rep_convex_principal less_set_def
   2.191 +by (fast intro: convex_le_refl elim: convex_le_trans)
   2.192 +
   2.193 +lemma convex_principal_mono:
   2.194 +  "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u"
   2.195 +by (rule convex_principal_less_iff [THEN iffD2])
   2.196 +
   2.197 +lemma compact_convex_principal: "compact (convex_principal t)"
   2.198 +by (rule convex_pd.compact_principal)
   2.199 +
   2.200 +lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   2.201 +by (induct ys rule: convex_pd.principal_induct, simp, simp)
   2.202 +
   2.203 +instance convex_pd :: (bifinite) pcpo
   2.204 +by (intro_classes, fast intro: convex_pd_minimal)
   2.205 +
   2.206 +lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
   2.207 +by (rule convex_pd_minimal [THEN UU_I, symmetric])
   2.208 +
   2.209 +
   2.210 +subsection {* Approximation *}
   2.211 +
   2.212 +instance convex_pd :: (bifinite) approx ..
   2.213 +
   2.214 +defs (overloaded)
   2.215 +  approx_convex_pd_def:
   2.216 +    "approx \<equiv> (\<lambda>n. convex_pd.basis_fun (\<lambda>t. convex_principal (approx_pd n t)))"
   2.217 +
   2.218 +lemma approx_convex_principal [simp]:
   2.219 +  "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
   2.220 +unfolding approx_convex_pd_def
   2.221 +apply (rule convex_pd.basis_fun_principal)
   2.222 +apply (erule convex_principal_mono [OF approx_pd_convex_mono])
   2.223 +done
   2.224 +
   2.225 +lemma chain_approx_convex_pd:
   2.226 +  "chain (approx :: nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd)"
   2.227 +unfolding approx_convex_pd_def
   2.228 +by (rule convex_pd.chain_basis_fun_take)
   2.229 +
   2.230 +lemma lub_approx_convex_pd:
   2.231 +  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a convex_pd)"
   2.232 +unfolding approx_convex_pd_def
   2.233 +by (rule convex_pd.lub_basis_fun_take)
   2.234 +
   2.235 +lemma approx_convex_pd_idem:
   2.236 +  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a convex_pd)"
   2.237 +apply (induct xs rule: convex_pd.principal_induct, simp)
   2.238 +apply (simp add: approx_pd_idem)
   2.239 +done
   2.240 +
   2.241 +lemma approx_eq_convex_principal:
   2.242 +  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
   2.243 +unfolding approx_convex_pd_def
   2.244 +by (rule convex_pd.basis_fun_take_eq_principal)
   2.245 +
   2.246 +lemma finite_fixes_approx_convex_pd:
   2.247 +  "finite {xs::'a convex_pd. approx n\<cdot>xs = xs}"
   2.248 +unfolding approx_convex_pd_def
   2.249 +by (rule convex_pd.finite_fixes_basis_fun_take)
   2.250 +
   2.251 +instance convex_pd :: (bifinite) bifinite
   2.252 +apply intro_classes
   2.253 +apply (simp add: chain_approx_convex_pd)
   2.254 +apply (rule lub_approx_convex_pd)
   2.255 +apply (rule approx_convex_pd_idem)
   2.256 +apply (rule finite_fixes_approx_convex_pd)
   2.257 +done
   2.258 +
   2.259 +lemma compact_imp_convex_principal:
   2.260 +  "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
   2.261 +apply (drule bifinite_compact_eq_approx)
   2.262 +apply (erule exE)
   2.263 +apply (erule subst)
   2.264 +apply (cut_tac n=i and xs=xs in approx_eq_convex_principal)
   2.265 +apply fast
   2.266 +done
   2.267 +
   2.268 +lemma convex_principal_induct:
   2.269 +  "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
   2.270 +apply (erule approx_induct, rename_tac xs)
   2.271 +apply (cut_tac n=n and xs=xs in approx_eq_convex_principal)
   2.272 +apply (clarify, simp)
   2.273 +done
   2.274 +
   2.275 +lemma convex_principal_induct2:
   2.276 +  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   2.277 +    \<And>t u. P (convex_principal t) (convex_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
   2.278 +apply (rule_tac x=ys in spec)
   2.279 +apply (rule_tac xs=xs in convex_principal_induct, simp)
   2.280 +apply (rule allI, rename_tac ys)
   2.281 +apply (rule_tac xs=ys in convex_principal_induct, simp)
   2.282 +apply simp
   2.283 +done
   2.284 +
   2.285 +
   2.286 +subsection {* Monadic unit *}
   2.287 +
   2.288 +definition
   2.289 +  convex_unit :: "'a \<rightarrow> 'a convex_pd" where
   2.290 +  "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
   2.291 +
   2.292 +lemma convex_unit_Rep_compact_basis [simp]:
   2.293 +  "convex_unit\<cdot>(Rep_compact_basis a) = convex_principal (PDUnit a)"
   2.294 +unfolding convex_unit_def
   2.295 +apply (rule compact_basis.basis_fun_principal)
   2.296 +apply (rule convex_principal_mono)
   2.297 +apply (erule PDUnit_convex_mono)
   2.298 +done
   2.299 +
   2.300 +lemma convex_unit_strict [simp]: "convex_unit\<cdot>\<bottom> = \<bottom>"
   2.301 +unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
   2.302 +
   2.303 +lemma approx_convex_unit [simp]:
   2.304 +  "approx n\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(approx n\<cdot>x)"
   2.305 +apply (induct x rule: compact_basis_induct, simp)
   2.306 +apply (simp add: approx_Rep_compact_basis)
   2.307 +done
   2.308 +
   2.309 +lemma convex_unit_less_iff [simp]:
   2.310 +  "(convex_unit\<cdot>x \<sqsubseteq> convex_unit\<cdot>y) = (x \<sqsubseteq> y)"
   2.311 + apply (rule iffI)
   2.312 +  apply (rule bifinite_less_ext)
   2.313 +  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   2.314 +  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.315 +  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   2.316 +  apply (clarify, simp add: compact_le_def)
   2.317 + apply (erule monofun_cfun_arg)
   2.318 +done
   2.319 +
   2.320 +lemma convex_unit_eq_iff [simp]:
   2.321 +  "(convex_unit\<cdot>x = convex_unit\<cdot>y) = (x = y)"
   2.322 +unfolding po_eq_conv by simp
   2.323 +
   2.324 +lemma convex_unit_strict_iff [simp]: "(convex_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   2.325 +unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
   2.326 +
   2.327 +lemma compact_convex_unit_iff [simp]:
   2.328 +  "compact (convex_unit\<cdot>x) = compact x"
   2.329 +unfolding bifinite_compact_iff by simp
   2.330 +
   2.331 +
   2.332 +subsection {* Monadic plus *}
   2.333 +
   2.334 +definition
   2.335 +  convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
   2.336 +  "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
   2.337 +      convex_principal (PDPlus t u)))"
   2.338 +
   2.339 +abbreviation
   2.340 +  convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
   2.341 +    (infixl "+\<natural>" 65) where
   2.342 +  "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
   2.343 +
   2.344 +lemma convex_plus_principal [simp]:
   2.345 +  "convex_plus\<cdot>(convex_principal t)\<cdot>(convex_principal u) =
   2.346 +   convex_principal (PDPlus t u)"
   2.347 +unfolding convex_plus_def
   2.348 +by (simp add: convex_pd.basis_fun_principal
   2.349 +    convex_pd.basis_fun_mono PDPlus_convex_mono)
   2.350 +
   2.351 +lemma approx_convex_plus [simp]:
   2.352 +  "approx n\<cdot>(convex_plus\<cdot>xs\<cdot>ys) = convex_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   2.353 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.354 +
   2.355 +lemma convex_plus_commute: "convex_plus\<cdot>xs\<cdot>ys = convex_plus\<cdot>ys\<cdot>xs"
   2.356 +apply (induct xs ys rule: convex_principal_induct2, simp, simp)
   2.357 +apply (simp add: PDPlus_commute)
   2.358 +done
   2.359 +
   2.360 +lemma convex_plus_assoc:
   2.361 +  "convex_plus\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>zs = convex_plus\<cdot>xs\<cdot>(convex_plus\<cdot>ys\<cdot>zs)"
   2.362 +apply (induct xs ys arbitrary: zs rule: convex_principal_induct2, simp, simp)
   2.363 +apply (rule_tac xs=zs in convex_principal_induct, simp)
   2.364 +apply (simp add: PDPlus_assoc)
   2.365 +done
   2.366 +
   2.367 +lemma convex_plus_absorb: "convex_plus\<cdot>xs\<cdot>xs = xs"
   2.368 +apply (induct xs rule: convex_principal_induct, simp)
   2.369 +apply (simp add: PDPlus_absorb)
   2.370 +done
   2.371 +
   2.372 +lemma convex_unit_less_plus_iff [simp]:
   2.373 +  "(convex_unit\<cdot>x \<sqsubseteq> convex_plus\<cdot>ys\<cdot>zs) =
   2.374 +   (convex_unit\<cdot>x \<sqsubseteq> ys \<and> convex_unit\<cdot>x \<sqsubseteq> zs)"
   2.375 + apply (rule iffI)
   2.376 +  apply (subgoal_tac
   2.377 +    "adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
   2.378 +   apply (drule admD [rule_format], rule chain_approx)
   2.379 +    apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.380 +    apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.381 +    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
   2.382 +    apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_convex_principal, simp)
   2.383 +    apply (clarify, simp)
   2.384 +   apply simp
   2.385 +  apply simp
   2.386 + apply (erule conjE)
   2.387 + apply (subst convex_plus_absorb [of "convex_unit\<cdot>x", symmetric])
   2.388 + apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   2.389 +done
   2.390 +
   2.391 +lemma convex_plus_less_unit_iff [simp]:
   2.392 +  "(convex_plus\<cdot>xs\<cdot>ys \<sqsubseteq> convex_unit\<cdot>z) =
   2.393 +   (xs \<sqsubseteq> convex_unit\<cdot>z \<and> ys \<sqsubseteq> convex_unit\<cdot>z)"
   2.394 + apply (rule iffI)
   2.395 +  apply (subgoal_tac
   2.396 +    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
   2.397 +   apply (drule admD [rule_format], rule chain_approx)
   2.398 +    apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.399 +    apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
   2.400 +    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
   2.401 +    apply (cut_tac x="approx i\<cdot>z" in compact_imp_Rep_compact_basis, simp)
   2.402 +    apply (clarify, simp)
   2.403 +   apply simp
   2.404 +  apply simp
   2.405 + apply (erule conjE)
   2.406 + apply (subst convex_plus_absorb [of "convex_unit\<cdot>z", symmetric])
   2.407 + apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   2.408 +done
   2.409 +
   2.410 +
   2.411 +subsection {* Induction rules *}
   2.412 +
   2.413 +lemma convex_pd_induct1:
   2.414 +  assumes P: "adm P"
   2.415 +  assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
   2.416 +  assumes insert:
   2.417 +    "\<And>x ys. \<lbrakk>P (convex_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>(convex_unit\<cdot>x)\<cdot>ys)"
   2.418 +  shows "P (xs::'a convex_pd)"
   2.419 +apply (induct xs rule: convex_principal_induct, rule P)
   2.420 +apply (induct_tac t rule: pd_basis_induct1)
   2.421 +apply (simp only: convex_unit_Rep_compact_basis [symmetric])
   2.422 +apply (rule unit)
   2.423 +apply (simp only: convex_unit_Rep_compact_basis [symmetric]
   2.424 +                  convex_plus_principal [symmetric])
   2.425 +apply (erule insert [OF unit])
   2.426 +done
   2.427 +
   2.428 +lemma convex_pd_induct:
   2.429 +  assumes P: "adm P"
   2.430 +  assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
   2.431 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>xs\<cdot>ys)"
   2.432 +  shows "P (xs::'a convex_pd)"
   2.433 +apply (induct xs rule: convex_principal_induct, rule P)
   2.434 +apply (induct_tac t rule: pd_basis_induct)
   2.435 +apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
   2.436 +apply (simp only: convex_plus_principal [symmetric] plus)
   2.437 +done
   2.438 +
   2.439 +
   2.440 +subsection {* Monadic bind *}
   2.441 +
   2.442 +definition
   2.443 +  convex_bind_basis ::
   2.444 +  "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   2.445 +  "convex_bind_basis = fold_pd
   2.446 +    (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   2.447 +    (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   2.448 +
   2.449 +lemma ACI_convex_bind: "ACIf (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   2.450 +apply unfold_locales
   2.451 +apply (simp add: convex_plus_commute)
   2.452 +apply (simp add: convex_plus_assoc)
   2.453 +apply (simp add: convex_plus_absorb eta_cfun)
   2.454 +done
   2.455 +
   2.456 +lemma convex_bind_basis_simps [simp]:
   2.457 +  "convex_bind_basis (PDUnit a) =
   2.458 +    (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   2.459 +  "convex_bind_basis (PDPlus t u) =
   2.460 +    (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
   2.461 +unfolding convex_bind_basis_def
   2.462 +apply -
   2.463 +apply (rule ACIf.fold_pd_PDUnit [OF ACI_convex_bind])
   2.464 +apply (rule ACIf.fold_pd_PDPlus [OF ACI_convex_bind])
   2.465 +done
   2.466 +
   2.467 +lemma monofun_LAM:
   2.468 +  "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
   2.469 +by (simp add: expand_cfun_less)
   2.470 +
   2.471 +lemma convex_bind_basis_mono:
   2.472 +  "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
   2.473 +apply (erule convex_le_induct)
   2.474 +apply (erule (1) trans_less)
   2.475 +apply (simp add: monofun_LAM compact_le_def monofun_cfun)
   2.476 +apply (simp add: monofun_LAM compact_le_def monofun_cfun)
   2.477 +done
   2.478 +
   2.479 +definition
   2.480 +  convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   2.481 +  "convex_bind = convex_pd.basis_fun convex_bind_basis"
   2.482 +
   2.483 +lemma convex_bind_principal [simp]:
   2.484 +  "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
   2.485 +unfolding convex_bind_def
   2.486 +apply (rule convex_pd.basis_fun_principal)
   2.487 +apply (erule convex_bind_basis_mono)
   2.488 +done
   2.489 +
   2.490 +lemma convex_bind_unit [simp]:
   2.491 +  "convex_bind\<cdot>(convex_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   2.492 +by (induct x rule: compact_basis_induct, simp, simp)
   2.493 +
   2.494 +lemma convex_bind_plus [simp]:
   2.495 +  "convex_bind\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   2.496 +   convex_plus\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>(convex_bind\<cdot>ys\<cdot>f)"
   2.497 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.498 +
   2.499 +lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   2.500 +unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
   2.501 +
   2.502 +
   2.503 +subsection {* Map and join *}
   2.504 +
   2.505 +definition
   2.506 +  convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
   2.507 +  "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_unit\<cdot>(f\<cdot>x)))"
   2.508 +
   2.509 +definition
   2.510 +  convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
   2.511 +  "convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   2.512 +
   2.513 +lemma convex_map_unit [simp]:
   2.514 +  "convex_map\<cdot>f\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(f\<cdot>x)"
   2.515 +unfolding convex_map_def by simp
   2.516 +
   2.517 +lemma convex_map_plus [simp]:
   2.518 +  "convex_map\<cdot>f\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
   2.519 +   convex_plus\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>(convex_map\<cdot>f\<cdot>ys)"
   2.520 +unfolding convex_map_def by simp
   2.521 +
   2.522 +lemma convex_join_unit [simp]:
   2.523 +  "convex_join\<cdot>(convex_unit\<cdot>xs) = xs"
   2.524 +unfolding convex_join_def by simp
   2.525 +
   2.526 +lemma convex_join_plus [simp]:
   2.527 +  "convex_join\<cdot>(convex_plus\<cdot>xss\<cdot>yss) =
   2.528 +   convex_plus\<cdot>(convex_join\<cdot>xss)\<cdot>(convex_join\<cdot>yss)"
   2.529 +unfolding convex_join_def by simp
   2.530 +
   2.531 +lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   2.532 +by (induct xs rule: convex_pd_induct, simp_all)
   2.533 +
   2.534 +lemma convex_map_map:
   2.535 +  "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   2.536 +by (induct xs rule: convex_pd_induct, simp_all)
   2.537 +
   2.538 +lemma convex_join_map_unit:
   2.539 +  "convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs"
   2.540 +by (induct xs rule: convex_pd_induct, simp_all)
   2.541 +
   2.542 +lemma convex_join_map_join:
   2.543 +  "convex_join\<cdot>(convex_map\<cdot>convex_join\<cdot>xsss) = convex_join\<cdot>(convex_join\<cdot>xsss)"
   2.544 +by (induct xsss rule: convex_pd_induct, simp_all)
   2.545 +
   2.546 +lemma convex_join_map_map:
   2.547 +  "convex_join\<cdot>(convex_map\<cdot>(convex_map\<cdot>f)\<cdot>xss) =
   2.548 +   convex_map\<cdot>f\<cdot>(convex_join\<cdot>xss)"
   2.549 +by (induct xss rule: convex_pd_induct, simp_all)
   2.550 +
   2.551 +lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   2.552 +by (induct xs rule: convex_pd_induct, simp_all)
   2.553 +
   2.554 +
   2.555 +subsection {* Conversions to other powerdomains *}
   2.556 +
   2.557 +text {* Convex to upper *}
   2.558 +
   2.559 +lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u"
   2.560 +unfolding convex_le_def by simp
   2.561 +
   2.562 +definition
   2.563 +  convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
   2.564 +  "convex_to_upper = convex_pd.basis_fun upper_principal"
   2.565 +
   2.566 +lemma convex_to_upper_principal [simp]:
   2.567 +  "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
   2.568 +unfolding convex_to_upper_def
   2.569 +apply (rule convex_pd.basis_fun_principal)
   2.570 +apply (rule upper_principal_mono)
   2.571 +apply (erule convex_le_imp_upper_le)
   2.572 +done
   2.573 +
   2.574 +lemma convex_to_upper_unit [simp]:
   2.575 +  "convex_to_upper\<cdot>(convex_unit\<cdot>x) = upper_unit\<cdot>x"
   2.576 +by (induct x rule: compact_basis_induct, simp, simp)
   2.577 +
   2.578 +lemma convex_to_upper_plus [simp]:
   2.579 +  "convex_to_upper\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
   2.580 +   upper_plus\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper\<cdot>ys)"
   2.581 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.582 +
   2.583 +lemma approx_convex_to_upper:
   2.584 +  "approx i\<cdot>(convex_to_upper\<cdot>xs) = convex_to_upper\<cdot>(approx i\<cdot>xs)"
   2.585 +by (induct xs rule: convex_pd_induct, simp, simp, simp)
   2.586 +
   2.587 +text {* Convex to lower *}
   2.588 +
   2.589 +lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u"
   2.590 +unfolding convex_le_def by simp
   2.591 +
   2.592 +definition
   2.593 +  convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
   2.594 +  "convex_to_lower = convex_pd.basis_fun lower_principal"
   2.595 +
   2.596 +lemma convex_to_lower_principal [simp]:
   2.597 +  "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
   2.598 +unfolding convex_to_lower_def
   2.599 +apply (rule convex_pd.basis_fun_principal)
   2.600 +apply (rule lower_principal_mono)
   2.601 +apply (erule convex_le_imp_lower_le)
   2.602 +done
   2.603 +
   2.604 +lemma convex_to_lower_unit [simp]:
   2.605 +  "convex_to_lower\<cdot>(convex_unit\<cdot>x) = lower_unit\<cdot>x"
   2.606 +by (induct x rule: compact_basis_induct, simp, simp)
   2.607 +
   2.608 +lemma convex_to_lower_plus [simp]:
   2.609 +  "convex_to_lower\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
   2.610 +   lower_plus\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower\<cdot>ys)"
   2.611 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.612 +
   2.613 +lemma approx_convex_to_lower:
   2.614 +  "approx i\<cdot>(convex_to_lower\<cdot>xs) = convex_to_lower\<cdot>(approx i\<cdot>xs)"
   2.615 +by (induct xs rule: convex_pd_induct, simp, simp, simp)
   2.616 +
   2.617 +text {* Ordering property *}
   2.618 +
   2.619 +lemma convex_pd_less_iff:
   2.620 +  "(xs \<sqsubseteq> ys) =
   2.621 +    (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
   2.622 +     convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
   2.623 + apply (safe elim!: monofun_cfun_arg)
   2.624 + apply (rule bifinite_less_ext)
   2.625 + apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.626 + apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.627 + apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
   2.628 + apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
   2.629 + apply clarify
   2.630 + apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
   2.631 +done
   2.632 +
   2.633 +end
     3.1 --- a/src/HOLCF/HOLCF.thy	Mon Jan 14 19:26:01 2008 +0100
     3.2 +++ b/src/HOLCF/HOLCF.thy	Mon Jan 14 19:26:41 2008 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  *)
     3.5  
     3.6  theory HOLCF
     3.7 -imports Sprod Ssum Up Lift Discrete One Tr Domain Main
     3.8 +imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Main
     3.9  uses
    3.10    "holcf_logic.ML"
    3.11    "Tools/cont_consts.ML"
    3.12 @@ -19,6 +19,8 @@
    3.13  
    3.14  begin
    3.15  
    3.16 +defaultsort pcpo
    3.17 +
    3.18  ML_setup {*
    3.19    change_simpset (fn simpset => simpset addSolver
    3.20      (mk_solver' "adm_tac" (fn ss =>
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/LowerPD.thy	Mon Jan 14 19:26:41 2008 +0100
     4.3 @@ -0,0 +1,538 @@
     4.4 +(*  Title:      HOLCF/LowerPD.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Brian Huffman
     4.7 +*)
     4.8 +
     4.9 +header {* Lower powerdomain *}
    4.10 +
    4.11 +theory LowerPD
    4.12 +imports CompactBasis
    4.13 +begin
    4.14 +
    4.15 +subsection {* Basis preorder *}
    4.16 +
    4.17 +definition
    4.18 +  lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<flat>" 50) where
    4.19 +  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. compact_le x y)"
    4.20 +
    4.21 +lemma lower_le_refl [simp]: "t \<le>\<flat> t"
    4.22 +unfolding lower_le_def by (fast intro: compact_le_refl)
    4.23 +
    4.24 +lemma lower_le_trans: "\<lbrakk>t \<le>\<flat> u; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> t \<le>\<flat> v"
    4.25 +unfolding lower_le_def
    4.26 +apply (rule ballI)
    4.27 +apply (drule (1) bspec, erule bexE)
    4.28 +apply (drule (1) bspec, erule bexE)
    4.29 +apply (erule rev_bexI)
    4.30 +apply (erule (1) compact_le_trans)
    4.31 +done
    4.32 +
    4.33 +interpretation lower_le: preorder [lower_le]
    4.34 +by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
    4.35 +
    4.36 +lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
    4.37 +unfolding lower_le_def Rep_PDUnit
    4.38 +by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv])
    4.39 +
    4.40 +lemma PDUnit_lower_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
    4.41 +unfolding lower_le_def Rep_PDUnit by fast
    4.42 +
    4.43 +lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
    4.44 +unfolding lower_le_def Rep_PDPlus by fast
    4.45 +
    4.46 +lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
    4.47 +unfolding lower_le_def Rep_PDPlus by (fast intro: compact_le_refl)
    4.48 +
    4.49 +lemma lower_le_PDUnit_PDUnit_iff [simp]:
    4.50 +  "(PDUnit a \<le>\<flat> PDUnit b) = compact_le a b"
    4.51 +unfolding lower_le_def Rep_PDUnit by fast
    4.52 +
    4.53 +lemma lower_le_PDUnit_PDPlus_iff:
    4.54 +  "(PDUnit a \<le>\<flat> PDPlus t u) = (PDUnit a \<le>\<flat> t \<or> PDUnit a \<le>\<flat> u)"
    4.55 +unfolding lower_le_def Rep_PDPlus Rep_PDUnit by fast
    4.56 +
    4.57 +lemma lower_le_PDPlus_iff: "(PDPlus t u \<le>\<flat> v) = (t \<le>\<flat> v \<and> u \<le>\<flat> v)"
    4.58 +unfolding lower_le_def Rep_PDPlus by fast
    4.59 +
    4.60 +lemma lower_le_induct [induct set: lower_le]:
    4.61 +  assumes le: "t \<le>\<flat> u"
    4.62 +  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    4.63 +  assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
    4.64 +  assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
    4.65 +  shows "P t u"
    4.66 +using le
    4.67 +apply (induct t arbitrary: u rule: pd_basis_induct)
    4.68 +apply (erule rev_mp)
    4.69 +apply (induct_tac u rule: pd_basis_induct)
    4.70 +apply (simp add: 1)
    4.71 +apply (simp add: lower_le_PDUnit_PDPlus_iff)
    4.72 +apply (simp add: 2)
    4.73 +apply (subst PDPlus_commute)
    4.74 +apply (simp add: 2)
    4.75 +apply (simp add: lower_le_PDPlus_iff 3)
    4.76 +done
    4.77 +
    4.78 +lemma approx_pd_lower_mono1:
    4.79 +  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<flat> approx_pd j t"
    4.80 +apply (induct t rule: pd_basis_induct)
    4.81 +apply (simp add: compact_approx_mono1)
    4.82 +apply (simp add: PDPlus_lower_mono)
    4.83 +done
    4.84 +
    4.85 +lemma approx_pd_lower_le: "approx_pd i t \<le>\<flat> t"
    4.86 +apply (induct t rule: pd_basis_induct)
    4.87 +apply (simp add: compact_approx_le)
    4.88 +apply (simp add: PDPlus_lower_mono)
    4.89 +done
    4.90 +
    4.91 +lemma approx_pd_lower_mono:
    4.92 +  "t \<le>\<flat> u \<Longrightarrow> approx_pd n t \<le>\<flat> approx_pd n u"
    4.93 +apply (erule lower_le_induct)
    4.94 +apply (simp add: compact_approx_mono)
    4.95 +apply (simp add: lower_le_PDUnit_PDPlus_iff)
    4.96 +apply (simp add: lower_le_PDPlus_iff)
    4.97 +done
    4.98 +
    4.99 +
   4.100 +subsection {* Type definition *}
   4.101 +
   4.102 +cpodef (open) 'a lower_pd =
   4.103 +  "{S::'a::bifinite pd_basis set. lower_le.ideal S}"
   4.104 +apply (simp add: lower_le.adm_ideal)
   4.105 +apply (fast intro: lower_le.ideal_principal)
   4.106 +done
   4.107 +
   4.108 +lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
   4.109 +by (rule Rep_lower_pd [simplified])
   4.110 +
   4.111 +lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
   4.112 +unfolding less_lower_pd_def less_set_def .
   4.113 +
   4.114 +
   4.115 +subsection {* Principal ideals *}
   4.116 +
   4.117 +definition
   4.118 +  lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
   4.119 +  "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
   4.120 +
   4.121 +lemma Rep_lower_principal:
   4.122 +  "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
   4.123 +unfolding lower_principal_def
   4.124 +apply (rule Abs_lower_pd_inverse [simplified])
   4.125 +apply (rule lower_le.ideal_principal)
   4.126 +done
   4.127 +
   4.128 +interpretation lower_pd:
   4.129 +  bifinite_basis [lower_le lower_principal Rep_lower_pd approx_pd]
   4.130 +apply unfold_locales
   4.131 +apply (rule ideal_Rep_lower_pd)
   4.132 +apply (rule cont_Rep_lower_pd)
   4.133 +apply (rule Rep_lower_principal)
   4.134 +apply (simp only: less_lower_pd_def less_set_def)
   4.135 +apply (rule approx_pd_lower_le)
   4.136 +apply (rule approx_pd_idem)
   4.137 +apply (erule approx_pd_lower_mono)
   4.138 +apply (rule approx_pd_lower_mono1, simp)
   4.139 +apply (rule finite_range_approx_pd)
   4.140 +apply (rule ex_approx_pd_eq)
   4.141 +done
   4.142 +
   4.143 +lemma lower_principal_less_iff [simp]:
   4.144 +  "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
   4.145 +unfolding less_lower_pd_def Rep_lower_principal less_set_def
   4.146 +by (fast intro: lower_le_refl elim: lower_le_trans)
   4.147 +
   4.148 +lemma lower_principal_mono:
   4.149 +  "t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
   4.150 +by (rule lower_principal_less_iff [THEN iffD2])
   4.151 +
   4.152 +lemma compact_lower_principal: "compact (lower_principal t)"
   4.153 +apply (rule compactI2)
   4.154 +apply (simp add: less_lower_pd_def)
   4.155 +apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
   4.156 +apply (simp add: Rep_lower_principal set_cpo_simps)
   4.157 +apply (simp add: subset_def)
   4.158 +apply (drule spec, drule mp, rule lower_le_refl)
   4.159 +apply (erule exE, rename_tac i)
   4.160 +apply (rule_tac x=i in exI)
   4.161 +apply clarify
   4.162 +apply (erule (1) lower_le.idealD3 [OF ideal_Rep_lower_pd])
   4.163 +done
   4.164 +
   4.165 +lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   4.166 +by (induct ys rule: lower_pd.principal_induct, simp, simp)
   4.167 +
   4.168 +instance lower_pd :: (bifinite) pcpo
   4.169 +by (intro_classes, fast intro: lower_pd_minimal)
   4.170 +
   4.171 +lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
   4.172 +by (rule lower_pd_minimal [THEN UU_I, symmetric])
   4.173 +
   4.174 +
   4.175 +subsection {* Approximation *}
   4.176 +
   4.177 +instance lower_pd :: (bifinite) approx ..
   4.178 +
   4.179 +defs (overloaded)
   4.180 +  approx_lower_pd_def:
   4.181 +    "approx \<equiv> (\<lambda>n. lower_pd.basis_fun (\<lambda>t. lower_principal (approx_pd n t)))"
   4.182 +
   4.183 +lemma approx_lower_principal [simp]:
   4.184 +  "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
   4.185 +unfolding approx_lower_pd_def
   4.186 +apply (rule lower_pd.basis_fun_principal)
   4.187 +apply (erule lower_principal_mono [OF approx_pd_lower_mono])
   4.188 +done
   4.189 +
   4.190 +lemma chain_approx_lower_pd:
   4.191 +  "chain (approx :: nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd)"
   4.192 +unfolding approx_lower_pd_def
   4.193 +by (rule lower_pd.chain_basis_fun_take)
   4.194 +
   4.195 +lemma lub_approx_lower_pd:
   4.196 +  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a lower_pd)"
   4.197 +unfolding approx_lower_pd_def
   4.198 +by (rule lower_pd.lub_basis_fun_take)
   4.199 +
   4.200 +lemma approx_lower_pd_idem:
   4.201 +  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a lower_pd)"
   4.202 +apply (induct xs rule: lower_pd.principal_induct, simp)
   4.203 +apply (simp add: approx_pd_idem)
   4.204 +done
   4.205 +
   4.206 +lemma approx_eq_lower_principal:
   4.207 +  "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
   4.208 +unfolding approx_lower_pd_def
   4.209 +by (rule lower_pd.basis_fun_take_eq_principal)
   4.210 +
   4.211 +lemma finite_fixes_approx_lower_pd:
   4.212 +  "finite {xs::'a lower_pd. approx n\<cdot>xs = xs}"
   4.213 +unfolding approx_lower_pd_def
   4.214 +by (rule lower_pd.finite_fixes_basis_fun_take)
   4.215 +
   4.216 +instance lower_pd :: (bifinite) bifinite
   4.217 +apply intro_classes
   4.218 +apply (simp add: chain_approx_lower_pd)
   4.219 +apply (rule lub_approx_lower_pd)
   4.220 +apply (rule approx_lower_pd_idem)
   4.221 +apply (rule finite_fixes_approx_lower_pd)
   4.222 +done
   4.223 +
   4.224 +lemma compact_imp_lower_principal:
   4.225 +  "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
   4.226 +apply (drule bifinite_compact_eq_approx)
   4.227 +apply (erule exE)
   4.228 +apply (erule subst)
   4.229 +apply (cut_tac n=i and xs=xs in approx_eq_lower_principal)
   4.230 +apply fast
   4.231 +done
   4.232 +
   4.233 +lemma lower_principal_induct:
   4.234 +  "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
   4.235 +apply (erule approx_induct, rename_tac xs)
   4.236 +apply (cut_tac n=n and xs=xs in approx_eq_lower_principal)
   4.237 +apply (clarify, simp)
   4.238 +done
   4.239 +
   4.240 +lemma lower_principal_induct2:
   4.241 +  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   4.242 +    \<And>t u. P (lower_principal t) (lower_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
   4.243 +apply (rule_tac x=ys in spec)
   4.244 +apply (rule_tac xs=xs in lower_principal_induct, simp)
   4.245 +apply (rule allI, rename_tac ys)
   4.246 +apply (rule_tac xs=ys in lower_principal_induct, simp)
   4.247 +apply simp
   4.248 +done
   4.249 +
   4.250 +
   4.251 +subsection {* Monadic unit *}
   4.252 +
   4.253 +definition
   4.254 +  lower_unit :: "'a \<rightarrow> 'a lower_pd" where
   4.255 +  "lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
   4.256 +
   4.257 +lemma lower_unit_Rep_compact_basis [simp]:
   4.258 +  "lower_unit\<cdot>(Rep_compact_basis a) = lower_principal (PDUnit a)"
   4.259 +unfolding lower_unit_def
   4.260 +apply (rule compact_basis.basis_fun_principal)
   4.261 +apply (rule lower_principal_mono)
   4.262 +apply (erule PDUnit_lower_mono)
   4.263 +done
   4.264 +
   4.265 +lemma lower_unit_strict [simp]: "lower_unit\<cdot>\<bottom> = \<bottom>"
   4.266 +unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
   4.267 +
   4.268 +lemma approx_lower_unit [simp]:
   4.269 +  "approx n\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(approx n\<cdot>x)"
   4.270 +apply (induct x rule: compact_basis_induct, simp)
   4.271 +apply (simp add: approx_Rep_compact_basis)
   4.272 +done
   4.273 +
   4.274 +lemma lower_unit_less_iff [simp]:
   4.275 +  "(lower_unit\<cdot>x \<sqsubseteq> lower_unit\<cdot>y) = (x \<sqsubseteq> y)"
   4.276 + apply (rule iffI)
   4.277 +  apply (rule bifinite_less_ext)
   4.278 +  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   4.279 +  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   4.280 +  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   4.281 +  apply (clarify, simp add: compact_le_def)
   4.282 + apply (erule monofun_cfun_arg)
   4.283 +done
   4.284 +
   4.285 +lemma lower_unit_eq_iff [simp]:
   4.286 +  "(lower_unit\<cdot>x = lower_unit\<cdot>y) = (x = y)"
   4.287 +unfolding po_eq_conv by simp
   4.288 +
   4.289 +lemma lower_unit_strict_iff [simp]: "(lower_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   4.290 +unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
   4.291 +
   4.292 +lemma compact_lower_unit_iff [simp]:
   4.293 +  "compact (lower_unit\<cdot>x) = compact x"
   4.294 +unfolding bifinite_compact_iff by simp
   4.295 +
   4.296 +
   4.297 +subsection {* Monadic plus *}
   4.298 +
   4.299 +definition
   4.300 +  lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
   4.301 +  "lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
   4.302 +      lower_principal (PDPlus t u)))"
   4.303 +
   4.304 +abbreviation
   4.305 +  lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
   4.306 +    (infixl "+\<flat>" 65) where
   4.307 +  "xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
   4.308 +
   4.309 +lemma lower_plus_principal [simp]:
   4.310 +  "lower_plus\<cdot>(lower_principal t)\<cdot>(lower_principal u) =
   4.311 +   lower_principal (PDPlus t u)"
   4.312 +unfolding lower_plus_def
   4.313 +by (simp add: lower_pd.basis_fun_principal
   4.314 +    lower_pd.basis_fun_mono PDPlus_lower_mono)
   4.315 +
   4.316 +lemma approx_lower_plus [simp]:
   4.317 +  "approx n\<cdot>(lower_plus\<cdot>xs\<cdot>ys) = lower_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   4.318 +by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   4.319 +
   4.320 +lemma lower_plus_commute: "lower_plus\<cdot>xs\<cdot>ys = lower_plus\<cdot>ys\<cdot>xs"
   4.321 +apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   4.322 +apply (simp add: PDPlus_commute)
   4.323 +done
   4.324 +
   4.325 +lemma lower_plus_assoc:
   4.326 +  "lower_plus\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>zs = lower_plus\<cdot>xs\<cdot>(lower_plus\<cdot>ys\<cdot>zs)"
   4.327 +apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
   4.328 +apply (rule_tac xs=zs in lower_principal_induct, simp)
   4.329 +apply (simp add: PDPlus_assoc)
   4.330 +done
   4.331 +
   4.332 +lemma lower_plus_absorb: "lower_plus\<cdot>xs\<cdot>xs = xs"
   4.333 +apply (induct xs rule: lower_principal_induct, simp)
   4.334 +apply (simp add: PDPlus_absorb)
   4.335 +done
   4.336 +
   4.337 +lemma lower_plus_less1: "xs \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
   4.338 +apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   4.339 +apply (simp add: PDPlus_lower_less)
   4.340 +done
   4.341 +
   4.342 +lemma lower_plus_less2: "ys \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
   4.343 +by (subst lower_plus_commute, rule lower_plus_less1)
   4.344 +
   4.345 +lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs"
   4.346 +apply (subst lower_plus_absorb [of zs, symmetric])
   4.347 +apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   4.348 +done
   4.349 +
   4.350 +lemma lower_plus_less_iff:
   4.351 +  "(lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs) = (xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs)"
   4.352 +apply safe
   4.353 +apply (erule trans_less [OF lower_plus_less1])
   4.354 +apply (erule trans_less [OF lower_plus_less2])
   4.355 +apply (erule (1) lower_plus_least)
   4.356 +done
   4.357 +
   4.358 +lemma lower_plus_strict_iff [simp]:
   4.359 +  "(lower_plus\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<and> ys = \<bottom>)"
   4.360 +apply safe
   4.361 +apply (rule UU_I, erule subst, rule lower_plus_less1)
   4.362 +apply (rule UU_I, erule subst, rule lower_plus_less2)
   4.363 +apply (rule lower_plus_absorb)
   4.364 +done
   4.365 +
   4.366 +lemma lower_plus_strict1 [simp]: "lower_plus\<cdot>\<bottom>\<cdot>ys = ys"
   4.367 +apply (rule antisym_less [OF _ lower_plus_less2])
   4.368 +apply (simp add: lower_plus_least)
   4.369 +done
   4.370 +
   4.371 +lemma lower_plus_strict2 [simp]: "lower_plus\<cdot>xs\<cdot>\<bottom> = xs"
   4.372 +apply (rule antisym_less [OF _ lower_plus_less1])
   4.373 +apply (simp add: lower_plus_least)
   4.374 +done
   4.375 +
   4.376 +lemma lower_unit_less_plus_iff:
   4.377 +  "(lower_unit\<cdot>x \<sqsubseteq> lower_plus\<cdot>ys\<cdot>zs) =
   4.378 +    (lower_unit\<cdot>x \<sqsubseteq> ys \<or> lower_unit\<cdot>x \<sqsubseteq> zs)"
   4.379 + apply (rule iffI)
   4.380 +  apply (subgoal_tac
   4.381 +    "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
   4.382 +   apply (drule admD [rule_format], rule chain_approx)
   4.383 +    apply (drule_tac f="approx i" in monofun_cfun_arg)
   4.384 +    apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   4.385 +    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
   4.386 +    apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_lower_principal, simp)
   4.387 +    apply (clarify, simp add: lower_le_PDUnit_PDPlus_iff)
   4.388 +   apply simp
   4.389 +  apply simp
   4.390 + apply (erule disjE)
   4.391 +  apply (erule trans_less [OF _ lower_plus_less1])
   4.392 + apply (erule trans_less [OF _ lower_plus_less2])
   4.393 +done
   4.394 +
   4.395 +lemmas lower_pd_less_simps =
   4.396 +  lower_unit_less_iff
   4.397 +  lower_plus_less_iff
   4.398 +  lower_unit_less_plus_iff
   4.399 +
   4.400 +
   4.401 +subsection {* Induction rules *}
   4.402 +
   4.403 +lemma lower_pd_induct1:
   4.404 +  assumes P: "adm P"
   4.405 +  assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
   4.406 +  assumes insert:
   4.407 +    "\<And>x ys. \<lbrakk>P (lower_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>(lower_unit\<cdot>x)\<cdot>ys)"
   4.408 +  shows "P (xs::'a lower_pd)"
   4.409 +apply (induct xs rule: lower_principal_induct, rule P)
   4.410 +apply (induct_tac t rule: pd_basis_induct1)
   4.411 +apply (simp only: lower_unit_Rep_compact_basis [symmetric])
   4.412 +apply (rule unit)
   4.413 +apply (simp only: lower_unit_Rep_compact_basis [symmetric]
   4.414 +                  lower_plus_principal [symmetric])
   4.415 +apply (erule insert [OF unit])
   4.416 +done
   4.417 +
   4.418 +lemma lower_pd_induct:
   4.419 +  assumes P: "adm P"
   4.420 +  assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
   4.421 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>xs\<cdot>ys)"
   4.422 +  shows "P (xs::'a lower_pd)"
   4.423 +apply (induct xs rule: lower_principal_induct, rule P)
   4.424 +apply (induct_tac t rule: pd_basis_induct)
   4.425 +apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
   4.426 +apply (simp only: lower_plus_principal [symmetric] plus)
   4.427 +done
   4.428 +
   4.429 +
   4.430 +subsection {* Monadic bind *}
   4.431 +
   4.432 +definition
   4.433 +  lower_bind_basis ::
   4.434 +  "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
   4.435 +  "lower_bind_basis = fold_pd
   4.436 +    (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   4.437 +    (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   4.438 +
   4.439 +lemma ACI_lower_bind: "ACIf (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   4.440 +apply unfold_locales
   4.441 +apply (simp add: lower_plus_commute)
   4.442 +apply (simp add: lower_plus_assoc)
   4.443 +apply (simp add: lower_plus_absorb eta_cfun)
   4.444 +done
   4.445 +
   4.446 +lemma lower_bind_basis_simps [simp]:
   4.447 +  "lower_bind_basis (PDUnit a) =
   4.448 +    (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   4.449 +  "lower_bind_basis (PDPlus t u) =
   4.450 +    (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
   4.451 +unfolding lower_bind_basis_def
   4.452 +apply -
   4.453 +apply (rule ACIf.fold_pd_PDUnit [OF ACI_lower_bind])
   4.454 +apply (rule ACIf.fold_pd_PDPlus [OF ACI_lower_bind])
   4.455 +done
   4.456 +
   4.457 +lemma lower_bind_basis_mono:
   4.458 +  "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
   4.459 +unfolding expand_cfun_less
   4.460 +apply (erule lower_le_induct, safe)
   4.461 +apply (simp add: compact_le_def monofun_cfun)
   4.462 +apply (simp add: rev_trans_less [OF lower_plus_less1])
   4.463 +apply (simp add: lower_plus_less_iff)
   4.464 +done
   4.465 +
   4.466 +definition
   4.467 +  lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
   4.468 +  "lower_bind = lower_pd.basis_fun lower_bind_basis"
   4.469 +
   4.470 +lemma lower_bind_principal [simp]:
   4.471 +  "lower_bind\<cdot>(lower_principal t) = lower_bind_basis t"
   4.472 +unfolding lower_bind_def
   4.473 +apply (rule lower_pd.basis_fun_principal)
   4.474 +apply (erule lower_bind_basis_mono)
   4.475 +done
   4.476 +
   4.477 +lemma lower_bind_unit [simp]:
   4.478 +  "lower_bind\<cdot>(lower_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   4.479 +by (induct x rule: compact_basis_induct, simp, simp)
   4.480 +
   4.481 +lemma lower_bind_plus [simp]:
   4.482 +  "lower_bind\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   4.483 +   lower_plus\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>(lower_bind\<cdot>ys\<cdot>f)"
   4.484 +by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   4.485 +
   4.486 +lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   4.487 +unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)
   4.488 +
   4.489 +
   4.490 +subsection {* Map and join *}
   4.491 +
   4.492 +definition
   4.493 +  lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
   4.494 +  "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_unit\<cdot>(f\<cdot>x)))"
   4.495 +
   4.496 +definition
   4.497 +  lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
   4.498 +  "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   4.499 +
   4.500 +lemma lower_map_unit [simp]:
   4.501 +  "lower_map\<cdot>f\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(f\<cdot>x)"
   4.502 +unfolding lower_map_def by simp
   4.503 +
   4.504 +lemma lower_map_plus [simp]:
   4.505 +  "lower_map\<cdot>f\<cdot>(lower_plus\<cdot>xs\<cdot>ys) =
   4.506 +   lower_plus\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>(lower_map\<cdot>f\<cdot>ys)"
   4.507 +unfolding lower_map_def by simp
   4.508 +
   4.509 +lemma lower_join_unit [simp]:
   4.510 +  "lower_join\<cdot>(lower_unit\<cdot>xs) = xs"
   4.511 +unfolding lower_join_def by simp
   4.512 +
   4.513 +lemma lower_join_plus [simp]:
   4.514 +  "lower_join\<cdot>(lower_plus\<cdot>xss\<cdot>yss) =
   4.515 +   lower_plus\<cdot>(lower_join\<cdot>xss)\<cdot>(lower_join\<cdot>yss)"
   4.516 +unfolding lower_join_def by simp
   4.517 +
   4.518 +lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   4.519 +by (induct xs rule: lower_pd_induct, simp_all)
   4.520 +
   4.521 +lemma lower_map_map:
   4.522 +  "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   4.523 +by (induct xs rule: lower_pd_induct, simp_all)
   4.524 +
   4.525 +lemma lower_join_map_unit:
   4.526 +  "lower_join\<cdot>(lower_map\<cdot>lower_unit\<cdot>xs) = xs"
   4.527 +by (induct xs rule: lower_pd_induct, simp_all)
   4.528 +
   4.529 +lemma lower_join_map_join:
   4.530 +  "lower_join\<cdot>(lower_map\<cdot>lower_join\<cdot>xsss) = lower_join\<cdot>(lower_join\<cdot>xsss)"
   4.531 +by (induct xsss rule: lower_pd_induct, simp_all)
   4.532 +
   4.533 +lemma lower_join_map_map:
   4.534 +  "lower_join\<cdot>(lower_map\<cdot>(lower_map\<cdot>f)\<cdot>xss) =
   4.535 +   lower_map\<cdot>f\<cdot>(lower_join\<cdot>xss)"
   4.536 +by (induct xss rule: lower_pd_induct, simp_all)
   4.537 +
   4.538 +lemma lower_map_approx: "lower_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   4.539 +by (induct xs rule: lower_pd_induct, simp_all)
   4.540 +
   4.541 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/UpperPD.thy	Mon Jan 14 19:26:41 2008 +0100
     5.3 @@ -0,0 +1,508 @@
     5.4 +(*  Title:      HOLCF/UpperPD.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Brian Huffman
     5.7 +*)
     5.8 +
     5.9 +header {* Upper powerdomain *}
    5.10 +
    5.11 +theory UpperPD
    5.12 +imports CompactBasis
    5.13 +begin
    5.14 +
    5.15 +subsection {* Basis preorder *}
    5.16 +
    5.17 +definition
    5.18 +  upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where
    5.19 +  "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. compact_le x y)"
    5.20 +
    5.21 +lemma upper_le_refl [simp]: "t \<le>\<sharp> t"
    5.22 +unfolding upper_le_def by (fast intro: compact_le_refl)
    5.23 +
    5.24 +lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v"
    5.25 +unfolding upper_le_def
    5.26 +apply (rule ballI)
    5.27 +apply (drule (1) bspec, erule bexE)
    5.28 +apply (drule (1) bspec, erule bexE)
    5.29 +apply (erule rev_bexI)
    5.30 +apply (erule (1) compact_le_trans)
    5.31 +done
    5.32 +
    5.33 +interpretation upper_le: preorder [upper_le]
    5.34 +by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
    5.35 +
    5.36 +lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
    5.37 +unfolding upper_le_def Rep_PDUnit by simp
    5.38 +
    5.39 +lemma PDUnit_upper_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y"
    5.40 +unfolding upper_le_def Rep_PDUnit by simp
    5.41 +
    5.42 +lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
    5.43 +unfolding upper_le_def Rep_PDPlus by fast
    5.44 +
    5.45 +lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
    5.46 +unfolding upper_le_def Rep_PDPlus by (fast intro: compact_le_refl)
    5.47 +
    5.48 +lemma upper_le_PDUnit_PDUnit_iff [simp]:
    5.49 +  "(PDUnit a \<le>\<sharp> PDUnit b) = compact_le a b"
    5.50 +unfolding upper_le_def Rep_PDUnit by fast
    5.51 +
    5.52 +lemma upper_le_PDPlus_PDUnit_iff:
    5.53 +  "(PDPlus t u \<le>\<sharp> PDUnit a) = (t \<le>\<sharp> PDUnit a \<or> u \<le>\<sharp> PDUnit a)"
    5.54 +unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast
    5.55 +
    5.56 +lemma upper_le_PDPlus_iff: "(t \<le>\<sharp> PDPlus u v) = (t \<le>\<sharp> u \<and> t \<le>\<sharp> v)"
    5.57 +unfolding upper_le_def Rep_PDPlus by fast
    5.58 +
    5.59 +lemma upper_le_induct [induct set: upper_le]:
    5.60 +  assumes le: "t \<le>\<sharp> u"
    5.61 +  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    5.62 +  assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
    5.63 +  assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
    5.64 +  shows "P t u"
    5.65 +using le apply (induct u arbitrary: t rule: pd_basis_induct)
    5.66 +apply (erule rev_mp)
    5.67 +apply (induct_tac t rule: pd_basis_induct)
    5.68 +apply (simp add: 1)
    5.69 +apply (simp add: upper_le_PDPlus_PDUnit_iff)
    5.70 +apply (simp add: 2)
    5.71 +apply (subst PDPlus_commute)
    5.72 +apply (simp add: 2)
    5.73 +apply (simp add: upper_le_PDPlus_iff 3)
    5.74 +done
    5.75 +
    5.76 +lemma approx_pd_upper_mono1:
    5.77 +  "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<sharp> approx_pd j t"
    5.78 +apply (induct t rule: pd_basis_induct)
    5.79 +apply (simp add: compact_approx_mono1)
    5.80 +apply (simp add: PDPlus_upper_mono)
    5.81 +done
    5.82 +
    5.83 +lemma approx_pd_upper_le: "approx_pd i t \<le>\<sharp> t"
    5.84 +apply (induct t rule: pd_basis_induct)
    5.85 +apply (simp add: compact_approx_le)
    5.86 +apply (simp add: PDPlus_upper_mono)
    5.87 +done
    5.88 +
    5.89 +lemma approx_pd_upper_mono:
    5.90 +  "t \<le>\<sharp> u \<Longrightarrow> approx_pd n t \<le>\<sharp> approx_pd n u"
    5.91 +apply (erule upper_le_induct)
    5.92 +apply (simp add: compact_approx_mono)
    5.93 +apply (simp add: upper_le_PDPlus_PDUnit_iff)
    5.94 +apply (simp add: upper_le_PDPlus_iff)
    5.95 +done
    5.96 +
    5.97 +
    5.98 +subsection {* Type definition *}
    5.99 +
   5.100 +cpodef (open) 'a upper_pd =
   5.101 +  "{S::'a::bifinite pd_basis set. upper_le.ideal S}"
   5.102 +apply (simp add: upper_le.adm_ideal)
   5.103 +apply (fast intro: upper_le.ideal_principal)
   5.104 +done
   5.105 +
   5.106 +lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
   5.107 +by (rule Rep_upper_pd [simplified])
   5.108 +
   5.109 +definition
   5.110 +  upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
   5.111 +  "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
   5.112 +
   5.113 +lemma Rep_upper_principal:
   5.114 +  "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
   5.115 +unfolding upper_principal_def
   5.116 +apply (rule Abs_upper_pd_inverse [simplified])
   5.117 +apply (rule upper_le.ideal_principal)
   5.118 +done
   5.119 +
   5.120 +interpretation upper_pd:
   5.121 +  bifinite_basis [upper_le upper_principal Rep_upper_pd approx_pd]
   5.122 +apply unfold_locales
   5.123 +apply (rule ideal_Rep_upper_pd)
   5.124 +apply (rule cont_Rep_upper_pd)
   5.125 +apply (rule Rep_upper_principal)
   5.126 +apply (simp only: less_upper_pd_def less_set_def)
   5.127 +apply (rule approx_pd_upper_le)
   5.128 +apply (rule approx_pd_idem)
   5.129 +apply (erule approx_pd_upper_mono)
   5.130 +apply (rule approx_pd_upper_mono1, simp)
   5.131 +apply (rule finite_range_approx_pd)
   5.132 +apply (rule ex_approx_pd_eq)
   5.133 +done
   5.134 +
   5.135 +lemma upper_principal_less_iff [simp]:
   5.136 +  "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
   5.137 +unfolding less_upper_pd_def Rep_upper_principal less_set_def
   5.138 +by (fast intro: upper_le_refl elim: upper_le_trans)
   5.139 +
   5.140 +lemma upper_principal_mono:
   5.141 +  "t \<le>\<sharp> u \<Longrightarrow> upper_principal t \<sqsubseteq> upper_principal u"
   5.142 +by (rule upper_pd.principal_mono)
   5.143 +
   5.144 +lemma compact_upper_principal: "compact (upper_principal t)"
   5.145 +by (rule upper_pd.compact_principal)
   5.146 +
   5.147 +lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
   5.148 +by (induct ys rule: upper_pd.principal_induct, simp, simp)
   5.149 +
   5.150 +instance upper_pd :: (bifinite) pcpo
   5.151 +by (intro_classes, fast intro: upper_pd_minimal)
   5.152 +
   5.153 +lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
   5.154 +by (rule upper_pd_minimal [THEN UU_I, symmetric])
   5.155 +
   5.156 +
   5.157 +subsection {* Approximation *}
   5.158 +
   5.159 +instance upper_pd :: (bifinite) approx ..
   5.160 +
   5.161 +defs (overloaded)
   5.162 +  approx_upper_pd_def:
   5.163 +    "approx \<equiv> (\<lambda>n. upper_pd.basis_fun (\<lambda>t. upper_principal (approx_pd n t)))"
   5.164 +
   5.165 +lemma approx_upper_principal [simp]:
   5.166 +  "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
   5.167 +unfolding approx_upper_pd_def
   5.168 +apply (rule upper_pd.basis_fun_principal)
   5.169 +apply (erule upper_principal_mono [OF approx_pd_upper_mono])
   5.170 +done
   5.171 +
   5.172 +lemma chain_approx_upper_pd:
   5.173 +  "chain (approx :: nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd)"
   5.174 +unfolding approx_upper_pd_def
   5.175 +by (rule upper_pd.chain_basis_fun_take)
   5.176 +
   5.177 +lemma lub_approx_upper_pd:
   5.178 +  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a upper_pd)"
   5.179 +unfolding approx_upper_pd_def
   5.180 +by (rule upper_pd.lub_basis_fun_take)
   5.181 +
   5.182 +lemma approx_upper_pd_idem:
   5.183 +  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a upper_pd)"
   5.184 +apply (induct xs rule: upper_pd.principal_induct, simp)
   5.185 +apply (simp add: approx_pd_idem)
   5.186 +done
   5.187 +
   5.188 +lemma approx_eq_upper_principal:
   5.189 +  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
   5.190 +unfolding approx_upper_pd_def
   5.191 +by (rule upper_pd.basis_fun_take_eq_principal)
   5.192 +
   5.193 +lemma finite_fixes_approx_upper_pd:
   5.194 +  "finite {xs::'a upper_pd. approx n\<cdot>xs = xs}"
   5.195 +unfolding approx_upper_pd_def
   5.196 +by (rule upper_pd.finite_fixes_basis_fun_take)
   5.197 +
   5.198 +instance upper_pd :: (bifinite) bifinite
   5.199 +apply intro_classes
   5.200 +apply (simp add: chain_approx_upper_pd)
   5.201 +apply (rule lub_approx_upper_pd)
   5.202 +apply (rule approx_upper_pd_idem)
   5.203 +apply (rule finite_fixes_approx_upper_pd)
   5.204 +done
   5.205 +
   5.206 +lemma compact_imp_upper_principal:
   5.207 +  "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
   5.208 +apply (drule bifinite_compact_eq_approx)
   5.209 +apply (erule exE)
   5.210 +apply (erule subst)
   5.211 +apply (cut_tac n=i and xs=xs in approx_eq_upper_principal)
   5.212 +apply fast
   5.213 +done
   5.214 +
   5.215 +lemma upper_principal_induct:
   5.216 +  "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"
   5.217 +apply (erule approx_induct, rename_tac xs)
   5.218 +apply (cut_tac n=n and xs=xs in approx_eq_upper_principal)
   5.219 +apply (clarify, simp)
   5.220 +done
   5.221 +
   5.222 +lemma upper_principal_induct2:
   5.223 +  "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   5.224 +    \<And>t u. P (upper_principal t) (upper_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
   5.225 +apply (rule_tac x=ys in spec)
   5.226 +apply (rule_tac xs=xs in upper_principal_induct, simp)
   5.227 +apply (rule allI, rename_tac ys)
   5.228 +apply (rule_tac xs=ys in upper_principal_induct, simp)
   5.229 +apply simp
   5.230 +done
   5.231 +
   5.232 +
   5.233 +subsection {* Monadic unit *}
   5.234 +
   5.235 +definition
   5.236 +  upper_unit :: "'a \<rightarrow> 'a upper_pd" where
   5.237 +  "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
   5.238 +
   5.239 +lemma upper_unit_Rep_compact_basis [simp]:
   5.240 +  "upper_unit\<cdot>(Rep_compact_basis a) = upper_principal (PDUnit a)"
   5.241 +unfolding upper_unit_def
   5.242 +apply (rule compact_basis.basis_fun_principal)
   5.243 +apply (rule upper_principal_mono)
   5.244 +apply (erule PDUnit_upper_mono)
   5.245 +done
   5.246 +
   5.247 +lemma upper_unit_strict [simp]: "upper_unit\<cdot>\<bottom> = \<bottom>"
   5.248 +unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
   5.249 +
   5.250 +lemma approx_upper_unit [simp]:
   5.251 +  "approx n\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(approx n\<cdot>x)"
   5.252 +apply (induct x rule: compact_basis_induct, simp)
   5.253 +apply (simp add: approx_Rep_compact_basis)
   5.254 +done
   5.255 +
   5.256 +lemma upper_unit_less_iff [simp]:
   5.257 +  "(upper_unit\<cdot>x \<sqsubseteq> upper_unit\<cdot>y) = (x \<sqsubseteq> y)"
   5.258 + apply (rule iffI)
   5.259 +  apply (rule bifinite_less_ext)
   5.260 +  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   5.261 +  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   5.262 +  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   5.263 +  apply (clarify, simp add: compact_le_def)
   5.264 + apply (erule monofun_cfun_arg)
   5.265 +done
   5.266 +
   5.267 +lemma upper_unit_eq_iff [simp]:
   5.268 +  "(upper_unit\<cdot>x = upper_unit\<cdot>y) = (x = y)"
   5.269 +unfolding po_eq_conv by simp
   5.270 +
   5.271 +lemma upper_unit_strict_iff [simp]: "(upper_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   5.272 +unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   5.273 +
   5.274 +lemma compact_upper_unit_iff [simp]:
   5.275 +  "compact (upper_unit\<cdot>x) = compact x"
   5.276 +unfolding bifinite_compact_iff by simp
   5.277 +
   5.278 +
   5.279 +subsection {* Monadic plus *}
   5.280 +
   5.281 +definition
   5.282 +  upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
   5.283 +  "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
   5.284 +      upper_principal (PDPlus t u)))"
   5.285 +
   5.286 +abbreviation
   5.287 +  upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
   5.288 +    (infixl "+\<sharp>" 65) where
   5.289 +  "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
   5.290 +
   5.291 +lemma upper_plus_principal [simp]:
   5.292 +  "upper_plus\<cdot>(upper_principal t)\<cdot>(upper_principal u) =
   5.293 +   upper_principal (PDPlus t u)"
   5.294 +unfolding upper_plus_def
   5.295 +by (simp add: upper_pd.basis_fun_principal
   5.296 +    upper_pd.basis_fun_mono PDPlus_upper_mono)
   5.297 +
   5.298 +lemma approx_upper_plus [simp]:
   5.299 +  "approx n\<cdot>(upper_plus\<cdot>xs\<cdot>ys) = upper_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   5.300 +by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   5.301 +
   5.302 +lemma upper_plus_commute: "upper_plus\<cdot>xs\<cdot>ys = upper_plus\<cdot>ys\<cdot>xs"
   5.303 +apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   5.304 +apply (simp add: PDPlus_commute)
   5.305 +done
   5.306 +
   5.307 +lemma upper_plus_assoc:
   5.308 +  "upper_plus\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>zs = upper_plus\<cdot>xs\<cdot>(upper_plus\<cdot>ys\<cdot>zs)"
   5.309 +apply (induct xs ys arbitrary: zs rule: upper_principal_induct2, simp, simp)
   5.310 +apply (rule_tac xs=zs in upper_principal_induct, simp)
   5.311 +apply (simp add: PDPlus_assoc)
   5.312 +done
   5.313 +
   5.314 +lemma upper_plus_absorb: "upper_plus\<cdot>xs\<cdot>xs = xs"
   5.315 +apply (induct xs rule: upper_principal_induct, simp)
   5.316 +apply (simp add: PDPlus_absorb)
   5.317 +done
   5.318 +
   5.319 +lemma upper_plus_less1: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> xs"
   5.320 +apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   5.321 +apply (simp add: PDPlus_upper_less)
   5.322 +done
   5.323 +
   5.324 +lemma upper_plus_less2: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> ys"
   5.325 +by (subst upper_plus_commute, rule upper_plus_less1)
   5.326 +
   5.327 +lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs"
   5.328 +apply (subst upper_plus_absorb [of xs, symmetric])
   5.329 +apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   5.330 +done
   5.331 +
   5.332 +lemma upper_less_plus_iff:
   5.333 +  "(xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs) = (xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs)"
   5.334 +apply safe
   5.335 +apply (erule trans_less [OF _ upper_plus_less1])
   5.336 +apply (erule trans_less [OF _ upper_plus_less2])
   5.337 +apply (erule (1) upper_plus_greatest)
   5.338 +done
   5.339 +
   5.340 +lemma upper_plus_strict1 [simp]: "upper_plus\<cdot>\<bottom>\<cdot>ys = \<bottom>"
   5.341 +by (rule UU_I, rule upper_plus_less1)
   5.342 +
   5.343 +lemma upper_plus_strict2 [simp]: "upper_plus\<cdot>xs\<cdot>\<bottom> = \<bottom>"
   5.344 +by (rule UU_I, rule upper_plus_less2)
   5.345 +
   5.346 +lemma upper_plus_less_unit_iff:
   5.347 +  "(upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> upper_unit\<cdot>z) =
   5.348 +    (xs \<sqsubseteq> upper_unit\<cdot>z \<or> ys \<sqsubseteq> upper_unit\<cdot>z)"
   5.349 + apply (rule iffI)
   5.350 +  apply (subgoal_tac
   5.351 +    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
   5.352 +   apply (drule admD [rule_format], rule chain_approx)
   5.353 +    apply (drule_tac f="approx i" in monofun_cfun_arg)
   5.354 +    apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
   5.355 +    apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)
   5.356 +    apply (cut_tac x="approx i\<cdot>z" in compact_imp_Rep_compact_basis, simp)
   5.357 +    apply (clarify, simp add: upper_le_PDPlus_PDUnit_iff)
   5.358 +   apply simp
   5.359 +  apply simp
   5.360 + apply (erule disjE)
   5.361 +  apply (erule trans_less [OF upper_plus_less1])
   5.362 + apply (erule trans_less [OF upper_plus_less2])
   5.363 +done
   5.364 +
   5.365 +lemmas upper_pd_less_simps =
   5.366 +  upper_unit_less_iff
   5.367 +  upper_less_plus_iff
   5.368 +  upper_plus_less_unit_iff
   5.369 +
   5.370 +
   5.371 +subsection {* Induction rules *}
   5.372 +
   5.373 +lemma upper_pd_induct1:
   5.374 +  assumes P: "adm P"
   5.375 +  assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
   5.376 +  assumes insert:
   5.377 +    "\<And>x ys. \<lbrakk>P (upper_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>(upper_unit\<cdot>x)\<cdot>ys)"
   5.378 +  shows "P (xs::'a upper_pd)"
   5.379 +apply (induct xs rule: upper_principal_induct, rule P)
   5.380 +apply (induct_tac t rule: pd_basis_induct1)
   5.381 +apply (simp only: upper_unit_Rep_compact_basis [symmetric])
   5.382 +apply (rule unit)
   5.383 +apply (simp only: upper_unit_Rep_compact_basis [symmetric]
   5.384 +                  upper_plus_principal [symmetric])
   5.385 +apply (erule insert [OF unit])
   5.386 +done
   5.387 +
   5.388 +lemma upper_pd_induct:
   5.389 +  assumes P: "adm P"
   5.390 +  assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
   5.391 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>xs\<cdot>ys)"
   5.392 +  shows "P (xs::'a upper_pd)"
   5.393 +apply (induct xs rule: upper_principal_induct, rule P)
   5.394 +apply (induct_tac t rule: pd_basis_induct)
   5.395 +apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
   5.396 +apply (simp only: upper_plus_principal [symmetric] plus)
   5.397 +done
   5.398 +
   5.399 +
   5.400 +subsection {* Monadic bind *}
   5.401 +
   5.402 +definition
   5.403 +  upper_bind_basis ::
   5.404 +  "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   5.405 +  "upper_bind_basis = fold_pd
   5.406 +    (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   5.407 +    (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   5.408 +
   5.409 +lemma ACI_upper_bind: "ACIf (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   5.410 +apply unfold_locales
   5.411 +apply (simp add: upper_plus_commute)
   5.412 +apply (simp add: upper_plus_assoc)
   5.413 +apply (simp add: upper_plus_absorb eta_cfun)
   5.414 +done
   5.415 +
   5.416 +lemma upper_bind_basis_simps [simp]:
   5.417 +  "upper_bind_basis (PDUnit a) =
   5.418 +    (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   5.419 +  "upper_bind_basis (PDPlus t u) =
   5.420 +    (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
   5.421 +unfolding upper_bind_basis_def
   5.422 +apply -
   5.423 +apply (rule ACIf.fold_pd_PDUnit [OF ACI_upper_bind])
   5.424 +apply (rule ACIf.fold_pd_PDPlus [OF ACI_upper_bind])
   5.425 +done
   5.426 +
   5.427 +lemma upper_bind_basis_mono:
   5.428 +  "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
   5.429 +unfolding expand_cfun_less
   5.430 +apply (erule upper_le_induct, safe)
   5.431 +apply (simp add: compact_le_def monofun_cfun)
   5.432 +apply (simp add: trans_less [OF upper_plus_less1])
   5.433 +apply (simp add: upper_less_plus_iff)
   5.434 +done
   5.435 +
   5.436 +definition
   5.437 +  upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   5.438 +  "upper_bind = upper_pd.basis_fun upper_bind_basis"
   5.439 +
   5.440 +lemma upper_bind_principal [simp]:
   5.441 +  "upper_bind\<cdot>(upper_principal t) = upper_bind_basis t"
   5.442 +unfolding upper_bind_def
   5.443 +apply (rule upper_pd.basis_fun_principal)
   5.444 +apply (erule upper_bind_basis_mono)
   5.445 +done
   5.446 +
   5.447 +lemma upper_bind_unit [simp]:
   5.448 +  "upper_bind\<cdot>(upper_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   5.449 +by (induct x rule: compact_basis_induct, simp, simp)
   5.450 +
   5.451 +lemma upper_bind_plus [simp]:
   5.452 +  "upper_bind\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   5.453 +   upper_plus\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>(upper_bind\<cdot>ys\<cdot>f)"
   5.454 +by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   5.455 +
   5.456 +lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   5.457 +unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)
   5.458 +
   5.459 +
   5.460 +subsection {* Map and join *}
   5.461 +
   5.462 +definition
   5.463 +  upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
   5.464 +  "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_unit\<cdot>(f\<cdot>x)))"
   5.465 +
   5.466 +definition
   5.467 +  upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   5.468 +  "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   5.469 +
   5.470 +lemma upper_map_unit [simp]:
   5.471 +  "upper_map\<cdot>f\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(f\<cdot>x)"
   5.472 +unfolding upper_map_def by simp
   5.473 +
   5.474 +lemma upper_map_plus [simp]:
   5.475 +  "upper_map\<cdot>f\<cdot>(upper_plus\<cdot>xs\<cdot>ys) =
   5.476 +   upper_plus\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>(upper_map\<cdot>f\<cdot>ys)"
   5.477 +unfolding upper_map_def by simp
   5.478 +
   5.479 +lemma upper_join_unit [simp]:
   5.480 +  "upper_join\<cdot>(upper_unit\<cdot>xs) = xs"
   5.481 +unfolding upper_join_def by simp
   5.482 +
   5.483 +lemma upper_join_plus [simp]:
   5.484 +  "upper_join\<cdot>(upper_plus\<cdot>xss\<cdot>yss) =
   5.485 +   upper_plus\<cdot>(upper_join\<cdot>xss)\<cdot>(upper_join\<cdot>yss)"
   5.486 +unfolding upper_join_def by simp
   5.487 +
   5.488 +lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   5.489 +by (induct xs rule: upper_pd_induct, simp_all)
   5.490 +
   5.491 +lemma upper_map_map:
   5.492 +  "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   5.493 +by (induct xs rule: upper_pd_induct, simp_all)
   5.494 +
   5.495 +lemma upper_join_map_unit:
   5.496 +  "upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs"
   5.497 +by (induct xs rule: upper_pd_induct, simp_all)
   5.498 +
   5.499 +lemma upper_join_map_join:
   5.500 +  "upper_join\<cdot>(upper_map\<cdot>upper_join\<cdot>xsss) = upper_join\<cdot>(upper_join\<cdot>xsss)"
   5.501 +by (induct xsss rule: upper_pd_induct, simp_all)
   5.502 +
   5.503 +lemma upper_join_map_map:
   5.504 +  "upper_join\<cdot>(upper_map\<cdot>(upper_map\<cdot>f)\<cdot>xss) =
   5.505 +   upper_map\<cdot>f\<cdot>(upper_join\<cdot>xss)"
   5.506 +by (induct xss rule: upper_pd_induct, simp_all)
   5.507 +
   5.508 +lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
   5.509 +by (induct xs rule: upper_pd_induct, simp_all)
   5.510 +
   5.511 +end