1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOLCF/ConvexPD.thy Mon Jan 14 19:26:41 2008 +0100
1.3 @@ -0,0 +1,630 @@
1.4 +(* Title: HOLCF/ConvexPD.thy
1.5 + ID: $Id$
1.6 + Author: Brian Huffman
1.7 +*)
1.8 +
1.9 +header {* Convex powerdomain *}
1.10 +
1.11 +theory ConvexPD
1.12 +imports UpperPD LowerPD
1.13 +begin
1.14 +
1.15 +subsection {* Basis preorder *}
1.16 +
1.17 +definition
1.18 + convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<natural>" 50) where
1.19 + "convex_le = (\<lambda>u v. u \<le>\<sharp> v \<and> u \<le>\<flat> v)"
1.20 +
1.21 +lemma convex_le_refl [simp]: "t \<le>\<natural> t"
1.22 +unfolding convex_le_def by (fast intro: upper_le_refl lower_le_refl)
1.23 +
1.24 +lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
1.25 +unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
1.26 +
1.27 +interpretation convex_le: preorder [convex_le]
1.28 +by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
1.29 +
1.30 +lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
1.31 +unfolding convex_le_def Rep_PDUnit by simp
1.32 +
1.33 +lemma PDUnit_convex_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y"
1.34 +unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono)
1.35 +
1.36 +lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v"
1.37 +unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
1.38 +
1.39 +lemma convex_le_PDUnit_PDUnit_iff [simp]:
1.40 + "(PDUnit a \<le>\<natural> PDUnit b) = compact_le a b"
1.41 +unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
1.42 +
1.43 +lemma convex_le_PDUnit_lemma1:
1.44 + "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. compact_le a b)"
1.45 +unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
1.46 +using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
1.47 +
1.48 +lemma convex_le_PDUnit_PDPlus_iff [simp]:
1.49 + "(PDUnit a \<le>\<natural> PDPlus t u) = (PDUnit a \<le>\<natural> t \<and> PDUnit a \<le>\<natural> u)"
1.50 +unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast
1.51 +
1.52 +lemma convex_le_PDUnit_lemma2:
1.53 + "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. compact_le a b)"
1.54 +unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit
1.55 +using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast
1.56 +
1.57 +lemma convex_le_PDPlus_PDUnit_iff [simp]:
1.58 + "(PDPlus t u \<le>\<natural> PDUnit a) = (t \<le>\<natural> PDUnit a \<and> u \<le>\<natural> PDUnit a)"
1.59 +unfolding convex_le_PDUnit_lemma2 Rep_PDPlus by fast
1.60 +
1.61 +lemma convex_le_PDPlus_lemma:
1.62 + assumes z: "PDPlus t u \<le>\<natural> z"
1.63 + shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w"
1.64 +proof (intro exI conjI)
1.65 + let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. compact_le a b}"
1.66 + let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. compact_le a b}"
1.67 + let ?v = "Abs_pd_basis ?A"
1.68 + let ?w = "Abs_pd_basis ?B"
1.69 + have Rep_v: "Rep_pd_basis ?v = ?A"
1.70 + apply (rule Abs_pd_basis_inverse)
1.71 + apply (rule Rep_pd_basis_nonempty [of t, folded ex_in_conv, THEN exE])
1.72 + apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify)
1.73 + apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE)
1.74 + apply (simp add: pd_basis_def)
1.75 + apply fast
1.76 + done
1.77 + have Rep_w: "Rep_pd_basis ?w = ?B"
1.78 + apply (rule Abs_pd_basis_inverse)
1.79 + apply (rule Rep_pd_basis_nonempty [of u, folded ex_in_conv, THEN exE])
1.80 + apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify)
1.81 + apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE)
1.82 + apply (simp add: pd_basis_def)
1.83 + apply fast
1.84 + done
1.85 + show "z = PDPlus ?v ?w"
1.86 + apply (insert z)
1.87 + apply (simp add: convex_le_def, erule conjE)
1.88 + apply (simp add: Rep_pd_basis_inject [symmetric] Rep_PDPlus)
1.89 + apply (simp add: Rep_v Rep_w)
1.90 + apply (rule equalityI)
1.91 + apply (rule subsetI)
1.92 + apply (simp only: upper_le_def)
1.93 + apply (drule (1) bspec, erule bexE)
1.94 + apply (simp add: Rep_PDPlus)
1.95 + apply fast
1.96 + apply fast
1.97 + done
1.98 + show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w"
1.99 + apply (insert z)
1.100 + apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w)
1.101 + apply fast+
1.102 + done
1.103 +qed
1.104 +
1.105 +lemma convex_le_induct [induct set: convex_le]:
1.106 + assumes le: "t \<le>\<natural> u"
1.107 + assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v"
1.108 + assumes 3: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
1.109 + assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
1.110 + shows "P t u"
1.111 +using le apply (induct t arbitrary: u rule: pd_basis_induct)
1.112 +apply (erule rev_mp)
1.113 +apply (induct_tac u rule: pd_basis_induct1)
1.114 +apply (simp add: 3)
1.115 +apply (simp, clarify, rename_tac a b t)
1.116 +apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)")
1.117 +apply (simp add: PDPlus_absorb)
1.118 +apply (erule (1) 4 [OF 3])
1.119 +apply (drule convex_le_PDPlus_lemma, clarify)
1.120 +apply (simp add: 4)
1.121 +done
1.122 +
1.123 +lemma approx_pd_convex_mono1:
1.124 + "i \<le> j \<Longrightarrow> approx_pd i t \<le>\<natural> approx_pd j t"
1.125 +apply (induct t rule: pd_basis_induct)
1.126 +apply (simp add: compact_approx_mono1)
1.127 +apply (simp add: PDPlus_convex_mono)
1.128 +done
1.129 +
1.130 +lemma approx_pd_convex_le: "approx_pd i t \<le>\<natural> t"
1.131 +apply (induct t rule: pd_basis_induct)
1.132 +apply (simp add: compact_approx_le)
1.133 +apply (simp add: PDPlus_convex_mono)
1.134 +done
1.135 +
1.136 +lemma approx_pd_convex_mono:
1.137 + "t \<le>\<natural> u \<Longrightarrow> approx_pd n t \<le>\<natural> approx_pd n u"
1.138 +apply (erule convex_le_induct)
1.139 +apply (erule (1) convex_le_trans)
1.140 +apply (simp add: compact_approx_mono)
1.141 +apply (simp add: PDPlus_convex_mono)
1.142 +done
1.143 +
1.144 +
1.145 +subsection {* Type definition *}
1.146 +
1.147 +cpodef (open) 'a convex_pd =
1.148 + "{S::'a::bifinite pd_basis set. convex_le.ideal S}"
1.149 +apply (simp add: convex_le.adm_ideal)
1.150 +apply (fast intro: convex_le.ideal_principal)
1.151 +done
1.152 +
1.153 +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
1.154 +by (rule Rep_convex_pd [simplified])
1.155 +
1.156 +lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
1.157 +unfolding less_convex_pd_def less_set_def .
1.158 +
1.159 +
1.160 +subsection {* Principal ideals *}
1.161 +
1.162 +definition
1.163 + convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
1.164 + "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
1.165 +
1.166 +lemma Rep_convex_principal:
1.167 + "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
1.168 +unfolding convex_principal_def
1.169 +apply (rule Abs_convex_pd_inverse [simplified])
1.170 +apply (rule convex_le.ideal_principal)
1.171 +done
1.172 +
1.173 +interpretation convex_pd:
1.174 + bifinite_basis [convex_le convex_principal Rep_convex_pd approx_pd]
1.175 +apply unfold_locales
1.176 +apply (rule ideal_Rep_convex_pd)
1.177 +apply (rule cont_Rep_convex_pd)
1.178 +apply (rule Rep_convex_principal)
1.179 +apply (simp only: less_convex_pd_def less_set_def)
1.180 +apply (rule approx_pd_convex_le)
1.181 +apply (rule approx_pd_idem)
1.182 +apply (erule approx_pd_convex_mono)
1.183 +apply (rule approx_pd_convex_mono1, simp)
1.184 +apply (rule finite_range_approx_pd)
1.185 +apply (rule ex_approx_pd_eq)
1.186 +done
1.187 +
1.188 +lemma convex_principal_less_iff [simp]:
1.189 + "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
1.190 +unfolding less_convex_pd_def Rep_convex_principal less_set_def
1.191 +by (fast intro: convex_le_refl elim: convex_le_trans)
1.192 +
1.193 +lemma convex_principal_mono:
1.194 + "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u"
1.195 +by (rule convex_principal_less_iff [THEN iffD2])
1.196 +
1.197 +lemma compact_convex_principal: "compact (convex_principal t)"
1.198 +by (rule convex_pd.compact_principal)
1.199 +
1.200 +lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
1.201 +by (induct ys rule: convex_pd.principal_induct, simp, simp)
1.202 +
1.203 +instance convex_pd :: (bifinite) pcpo
1.204 +by (intro_classes, fast intro: convex_pd_minimal)
1.205 +
1.206 +lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
1.207 +by (rule convex_pd_minimal [THEN UU_I, symmetric])
1.208 +
1.209 +
1.210 +subsection {* Approximation *}
1.211 +
1.212 +instance convex_pd :: (bifinite) approx ..
1.213 +
1.214 +defs (overloaded)
1.215 + approx_convex_pd_def:
1.216 + "approx \<equiv> (\<lambda>n. convex_pd.basis_fun (\<lambda>t. convex_principal (approx_pd n t)))"
1.217 +
1.218 +lemma approx_convex_principal [simp]:
1.219 + "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
1.220 +unfolding approx_convex_pd_def
1.221 +apply (rule convex_pd.basis_fun_principal)
1.222 +apply (erule convex_principal_mono [OF approx_pd_convex_mono])
1.223 +done
1.224 +
1.225 +lemma chain_approx_convex_pd:
1.226 + "chain (approx :: nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd)"
1.227 +unfolding approx_convex_pd_def
1.228 +by (rule convex_pd.chain_basis_fun_take)
1.229 +
1.230 +lemma lub_approx_convex_pd:
1.231 + "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a convex_pd)"
1.232 +unfolding approx_convex_pd_def
1.233 +by (rule convex_pd.lub_basis_fun_take)
1.234 +
1.235 +lemma approx_convex_pd_idem:
1.236 + "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a convex_pd)"
1.237 +apply (induct xs rule: convex_pd.principal_induct, simp)
1.238 +apply (simp add: approx_pd_idem)
1.239 +done
1.240 +
1.241 +lemma approx_eq_convex_principal:
1.242 + "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
1.243 +unfolding approx_convex_pd_def
1.244 +by (rule convex_pd.basis_fun_take_eq_principal)
1.245 +
1.246 +lemma finite_fixes_approx_convex_pd:
1.247 + "finite {xs::'a convex_pd. approx n\<cdot>xs = xs}"
1.248 +unfolding approx_convex_pd_def
1.249 +by (rule convex_pd.finite_fixes_basis_fun_take)
1.250 +
1.251 +instance convex_pd :: (bifinite) bifinite
1.252 +apply intro_classes
1.253 +apply (simp add: chain_approx_convex_pd)
1.254 +apply (rule lub_approx_convex_pd)
1.255 +apply (rule approx_convex_pd_idem)
1.256 +apply (rule finite_fixes_approx_convex_pd)
1.257 +done
1.258 +
1.259 +lemma compact_imp_convex_principal:
1.260 + "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
1.261 +apply (drule bifinite_compact_eq_approx)
1.262 +apply (erule exE)
1.263 +apply (erule subst)
1.264 +apply (cut_tac n=i and xs=xs in approx_eq_convex_principal)
1.265 +apply fast
1.266 +done
1.267 +
1.268 +lemma convex_principal_induct:
1.269 + "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
1.270 +apply (erule approx_induct, rename_tac xs)
1.271 +apply (cut_tac n=n and xs=xs in approx_eq_convex_principal)
1.272 +apply (clarify, simp)
1.273 +done
1.274 +
1.275 +lemma convex_principal_induct2:
1.276 + "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
1.277 + \<And>t u. P (convex_principal t) (convex_principal u)\<rbrakk> \<Longrightarrow> P xs ys"
1.278 +apply (rule_tac x=ys in spec)
1.279 +apply (rule_tac xs=xs in convex_principal_induct, simp)
1.280 +apply (rule allI, rename_tac ys)
1.281 +apply (rule_tac xs=ys in convex_principal_induct, simp)
1.282 +apply simp
1.283 +done
1.284 +
1.285 +
1.286 +subsection {* Monadic unit *}
1.287 +
1.288 +definition
1.289 + convex_unit :: "'a \<rightarrow> 'a convex_pd" where
1.290 + "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
1.291 +
1.292 +lemma convex_unit_Rep_compact_basis [simp]:
1.293 + "convex_unit\<cdot>(Rep_compact_basis a) = convex_principal (PDUnit a)"
1.294 +unfolding convex_unit_def
1.295 +apply (rule compact_basis.basis_fun_principal)
1.296 +apply (rule convex_principal_mono)
1.297 +apply (erule PDUnit_convex_mono)
1.298 +done
1.299 +
1.300 +lemma convex_unit_strict [simp]: "convex_unit\<cdot>\<bottom> = \<bottom>"
1.301 +unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
1.302 +
1.303 +lemma approx_convex_unit [simp]:
1.304 + "approx n\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(approx n\<cdot>x)"
1.305 +apply (induct x rule: compact_basis_induct, simp)
1.306 +apply (simp add: approx_Rep_compact_basis)
1.307 +done
1.308 +
1.309 +lemma convex_unit_less_iff [simp]:
1.310 + "(convex_unit\<cdot>x \<sqsubseteq> convex_unit\<cdot>y) = (x \<sqsubseteq> y)"
1.311 + apply (rule iffI)
1.312 + apply (rule bifinite_less_ext)
1.313 + apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
1.314 + apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
1.315 + apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
1.316 + apply (clarify, simp add: compact_le_def)
1.317 + apply (erule monofun_cfun_arg)
1.318 +done
1.319 +
1.320 +lemma convex_unit_eq_iff [simp]:
1.321 + "(convex_unit\<cdot>x = convex_unit\<cdot>y) = (x = y)"
1.322 +unfolding po_eq_conv by simp
1.323 +
1.324 +lemma convex_unit_strict_iff [simp]: "(convex_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
1.325 +unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
1.326 +
1.327 +lemma compact_convex_unit_iff [simp]:
1.328 + "compact (convex_unit\<cdot>x) = compact x"
1.329 +unfolding bifinite_compact_iff by simp
1.330 +
1.331 +
1.332 +subsection {* Monadic plus *}
1.333 +
1.334 +definition
1.335 + convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
1.336 + "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
1.337 + convex_principal (PDPlus t u)))"
1.338 +
1.339 +abbreviation
1.340 + convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
1.341 + (infixl "+\<natural>" 65) where
1.342 + "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
1.343 +
1.344 +lemma convex_plus_principal [simp]:
1.345 + "convex_plus\<cdot>(convex_principal t)\<cdot>(convex_principal u) =
1.346 + convex_principal (PDPlus t u)"
1.347 +unfolding convex_plus_def
1.348 +by (simp add: convex_pd.basis_fun_principal
1.349 + convex_pd.basis_fun_mono PDPlus_convex_mono)
1.350 +
1.351 +lemma approx_convex_plus [simp]:
1.352 + "approx n\<cdot>(convex_plus\<cdot>xs\<cdot>ys) = convex_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
1.353 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
1.354 +
1.355 +lemma convex_plus_commute: "convex_plus\<cdot>xs\<cdot>ys = convex_plus\<cdot>ys\<cdot>xs"
1.356 +apply (induct xs ys rule: convex_principal_induct2, simp, simp)
1.357 +apply (simp add: PDPlus_commute)
1.358 +done
1.359 +
1.360 +lemma convex_plus_assoc:
1.361 + "convex_plus\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>zs = convex_plus\<cdot>xs\<cdot>(convex_plus\<cdot>ys\<cdot>zs)"
1.362 +apply (induct xs ys arbitrary: zs rule: convex_principal_induct2, simp, simp)
1.363 +apply (rule_tac xs=zs in convex_principal_induct, simp)
1.364 +apply (simp add: PDPlus_assoc)
1.365 +done
1.366 +
1.367 +lemma convex_plus_absorb: "convex_plus\<cdot>xs\<cdot>xs = xs"
1.368 +apply (induct xs rule: convex_principal_induct, simp)
1.369 +apply (simp add: PDPlus_absorb)
1.370 +done
1.371 +
1.372 +lemma convex_unit_less_plus_iff [simp]:
1.373 + "(convex_unit\<cdot>x \<sqsubseteq> convex_plus\<cdot>ys\<cdot>zs) =
1.374 + (convex_unit\<cdot>x \<sqsubseteq> ys \<and> convex_unit\<cdot>x \<sqsubseteq> zs)"
1.375 + apply (rule iffI)
1.376 + apply (subgoal_tac
1.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)")
1.378 + apply (drule admD [rule_format], rule chain_approx)
1.379 + apply (drule_tac f="approx i" in monofun_cfun_arg)
1.380 + apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
1.381 + apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
1.382 + apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_convex_principal, simp)
1.383 + apply (clarify, simp)
1.384 + apply simp
1.385 + apply simp
1.386 + apply (erule conjE)
1.387 + apply (subst convex_plus_absorb [of "convex_unit\<cdot>x", symmetric])
1.388 + apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
1.389 +done
1.390 +
1.391 +lemma convex_plus_less_unit_iff [simp]:
1.392 + "(convex_plus\<cdot>xs\<cdot>ys \<sqsubseteq> convex_unit\<cdot>z) =
1.393 + (xs \<sqsubseteq> convex_unit\<cdot>z \<and> ys \<sqsubseteq> convex_unit\<cdot>z)"
1.394 + apply (rule iffI)
1.395 + apply (subgoal_tac
1.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))")
1.397 + apply (drule admD [rule_format], rule chain_approx)
1.398 + apply (drule_tac f="approx i" in monofun_cfun_arg)
1.399 + apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
1.400 + apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
1.401 + apply (cut_tac x="approx i\<cdot>z" in compact_imp_Rep_compact_basis, simp)
1.402 + apply (clarify, simp)
1.403 + apply simp
1.404 + apply simp
1.405 + apply (erule conjE)
1.406 + apply (subst convex_plus_absorb [of "convex_unit\<cdot>z", symmetric])
1.407 + apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
1.408 +done
1.409 +
1.410 +
1.411 +subsection {* Induction rules *}
1.412 +
1.413 +lemma convex_pd_induct1:
1.414 + assumes P: "adm P"
1.415 + assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
1.416 + assumes insert:
1.417 + "\<And>x ys. \<lbrakk>P (convex_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>(convex_unit\<cdot>x)\<cdot>ys)"
1.418 + shows "P (xs::'a convex_pd)"
1.419 +apply (induct xs rule: convex_principal_induct, rule P)
1.420 +apply (induct_tac t rule: pd_basis_induct1)
1.421 +apply (simp only: convex_unit_Rep_compact_basis [symmetric])
1.422 +apply (rule unit)
1.423 +apply (simp only: convex_unit_Rep_compact_basis [symmetric]
1.424 + convex_plus_principal [symmetric])
1.425 +apply (erule insert [OF unit])
1.426 +done
1.427 +
1.428 +lemma convex_pd_induct:
1.429 + assumes P: "adm P"
1.430 + assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
1.431 + assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>xs\<cdot>ys)"
1.432 + shows "P (xs::'a convex_pd)"
1.433 +apply (induct xs rule: convex_principal_induct, rule P)
1.434 +apply (induct_tac t rule: pd_basis_induct)
1.435 +apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
1.436 +apply (simp only: convex_plus_principal [symmetric] plus)
1.437 +done
1.438 +
1.439 +
1.440 +subsection {* Monadic bind *}
1.441 +
1.442 +definition
1.443 + convex_bind_basis ::
1.444 + "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
1.445 + "convex_bind_basis = fold_pd
1.446 + (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
1.447 + (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
1.448 +
1.449 +lemma ACI_convex_bind: "ACIf (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
1.450 +apply unfold_locales
1.451 +apply (simp add: convex_plus_commute)
1.452 +apply (simp add: convex_plus_assoc)
1.453 +apply (simp add: convex_plus_absorb eta_cfun)
1.454 +done
1.455 +
1.456 +lemma convex_bind_basis_simps [simp]:
1.457 + "convex_bind_basis (PDUnit a) =
1.458 + (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
1.459 + "convex_bind_basis (PDPlus t u) =
1.460 + (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
1.461 +unfolding convex_bind_basis_def
1.462 +apply -
1.463 +apply (rule ACIf.fold_pd_PDUnit [OF ACI_convex_bind])
1.464 +apply (rule ACIf.fold_pd_PDPlus [OF ACI_convex_bind])
1.465 +done
1.466 +
1.467 +lemma monofun_LAM:
1.468 + "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
1.469 +by (simp add: expand_cfun_less)
1.470 +
1.471 +lemma convex_bind_basis_mono:
1.472 + "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
1.473 +apply (erule convex_le_induct)
1.474 +apply (erule (1) trans_less)
1.475 +apply (simp add: monofun_LAM compact_le_def monofun_cfun)
1.476 +apply (simp add: monofun_LAM compact_le_def monofun_cfun)
1.477 +done
1.478 +
1.479 +definition
1.480 + convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
1.481 + "convex_bind = convex_pd.basis_fun convex_bind_basis"
1.482 +
1.483 +lemma convex_bind_principal [simp]:
1.484 + "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
1.485 +unfolding convex_bind_def
1.486 +apply (rule convex_pd.basis_fun_principal)
1.487 +apply (erule convex_bind_basis_mono)
1.488 +done
1.489 +
1.490 +lemma convex_bind_unit [simp]:
1.491 + "convex_bind\<cdot>(convex_unit\<cdot>x)\<cdot>f = f\<cdot>x"
1.492 +by (induct x rule: compact_basis_induct, simp, simp)
1.493 +
1.494 +lemma convex_bind_plus [simp]:
1.495 + "convex_bind\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>f =
1.496 + convex_plus\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>(convex_bind\<cdot>ys\<cdot>f)"
1.497 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
1.498 +
1.499 +lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
1.500 +unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
1.501 +
1.502 +
1.503 +subsection {* Map and join *}
1.504 +
1.505 +definition
1.506 + convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
1.507 + "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_unit\<cdot>(f\<cdot>x)))"
1.508 +
1.509 +definition
1.510 + convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
1.511 + "convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
1.512 +
1.513 +lemma convex_map_unit [simp]:
1.514 + "convex_map\<cdot>f\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(f\<cdot>x)"
1.515 +unfolding convex_map_def by simp
1.516 +
1.517 +lemma convex_map_plus [simp]:
1.518 + "convex_map\<cdot>f\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
1.519 + convex_plus\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>(convex_map\<cdot>f\<cdot>ys)"
1.520 +unfolding convex_map_def by simp
1.521 +
1.522 +lemma convex_join_unit [simp]:
1.523 + "convex_join\<cdot>(convex_unit\<cdot>xs) = xs"
1.524 +unfolding convex_join_def by simp
1.525 +
1.526 +lemma convex_join_plus [simp]:
1.527 + "convex_join\<cdot>(convex_plus\<cdot>xss\<cdot>yss) =
1.528 + convex_plus\<cdot>(convex_join\<cdot>xss)\<cdot>(convex_join\<cdot>yss)"
1.529 +unfolding convex_join_def by simp
1.530 +
1.531 +lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
1.532 +by (induct xs rule: convex_pd_induct, simp_all)
1.533 +
1.534 +lemma convex_map_map:
1.535 + "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
1.536 +by (induct xs rule: convex_pd_induct, simp_all)
1.537 +
1.538 +lemma convex_join_map_unit:
1.539 + "convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs"
1.540 +by (induct xs rule: convex_pd_induct, simp_all)
1.541 +
1.542 +lemma convex_join_map_join:
1.543 + "convex_join\<cdot>(convex_map\<cdot>convex_join\<cdot>xsss) = convex_join\<cdot>(convex_join\<cdot>xsss)"
1.544 +by (induct xsss rule: convex_pd_induct, simp_all)
1.545 +
1.546 +lemma convex_join_map_map:
1.547 + "convex_join\<cdot>(convex_map\<cdot>(convex_map\<cdot>f)\<cdot>xss) =
1.548 + convex_map\<cdot>f\<cdot>(convex_join\<cdot>xss)"
1.549 +by (induct xss rule: convex_pd_induct, simp_all)
1.550 +
1.551 +lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
1.552 +by (induct xs rule: convex_pd_induct, simp_all)
1.553 +
1.554 +
1.555 +subsection {* Conversions to other powerdomains *}
1.556 +
1.557 +text {* Convex to upper *}
1.558 +
1.559 +lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u"
1.560 +unfolding convex_le_def by simp
1.561 +
1.562 +definition
1.563 + convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
1.564 + "convex_to_upper = convex_pd.basis_fun upper_principal"
1.565 +
1.566 +lemma convex_to_upper_principal [simp]:
1.567 + "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
1.568 +unfolding convex_to_upper_def
1.569 +apply (rule convex_pd.basis_fun_principal)
1.570 +apply (rule upper_principal_mono)
1.571 +apply (erule convex_le_imp_upper_le)
1.572 +done
1.573 +
1.574 +lemma convex_to_upper_unit [simp]:
1.575 + "convex_to_upper\<cdot>(convex_unit\<cdot>x) = upper_unit\<cdot>x"
1.576 +by (induct x rule: compact_basis_induct, simp, simp)
1.577 +
1.578 +lemma convex_to_upper_plus [simp]:
1.579 + "convex_to_upper\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
1.580 + upper_plus\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper\<cdot>ys)"
1.581 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
1.582 +
1.583 +lemma approx_convex_to_upper:
1.584 + "approx i\<cdot>(convex_to_upper\<cdot>xs) = convex_to_upper\<cdot>(approx i\<cdot>xs)"
1.585 +by (induct xs rule: convex_pd_induct, simp, simp, simp)
1.586 +
1.587 +text {* Convex to lower *}
1.588 +
1.589 +lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u"
1.590 +unfolding convex_le_def by simp
1.591 +
1.592 +definition
1.593 + convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
1.594 + "convex_to_lower = convex_pd.basis_fun lower_principal"
1.595 +
1.596 +lemma convex_to_lower_principal [simp]:
1.597 + "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
1.598 +unfolding convex_to_lower_def
1.599 +apply (rule convex_pd.basis_fun_principal)
1.600 +apply (rule lower_principal_mono)
1.601 +apply (erule convex_le_imp_lower_le)
1.602 +done
1.603 +
1.604 +lemma convex_to_lower_unit [simp]:
1.605 + "convex_to_lower\<cdot>(convex_unit\<cdot>x) = lower_unit\<cdot>x"
1.606 +by (induct x rule: compact_basis_induct, simp, simp)
1.607 +
1.608 +lemma convex_to_lower_plus [simp]:
1.609 + "convex_to_lower\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
1.610 + lower_plus\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower\<cdot>ys)"
1.611 +by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
1.612 +
1.613 +lemma approx_convex_to_lower:
1.614 + "approx i\<cdot>(convex_to_lower\<cdot>xs) = convex_to_lower\<cdot>(approx i\<cdot>xs)"
1.615 +by (induct xs rule: convex_pd_induct, simp, simp, simp)
1.616 +
1.617 +text {* Ordering property *}
1.618 +
1.619 +lemma convex_pd_less_iff:
1.620 + "(xs \<sqsubseteq> ys) =
1.621 + (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
1.622 + convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
1.623 + apply (safe elim!: monofun_cfun_arg)
1.624 + apply (rule bifinite_less_ext)
1.625 + apply (drule_tac f="approx i" in monofun_cfun_arg)
1.626 + apply (drule_tac f="approx i" in monofun_cfun_arg)
1.627 + apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
1.628 + apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
1.629 + apply clarify
1.630 + apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
1.631 +done
1.632 +
1.633 +end