1(* Title: HOL/HOLCF/ConvexPD.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Convex powerdomain\<close> 6 7theory ConvexPD 8imports UpperPD LowerPD 9begin 10 11subsection \<open>Basis preorder\<close> 12 13definition 14 convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<natural>" 50) where 15 "convex_le = (\<lambda>u v. u \<le>\<sharp> v \<and> u \<le>\<flat> v)" 16 17lemma convex_le_refl [simp]: "t \<le>\<natural> t" 18unfolding convex_le_def by (fast intro: upper_le_refl lower_le_refl) 19 20lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v" 21unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans) 22 23interpretation convex_le: preorder convex_le 24by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans) 25 26lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t" 27unfolding convex_le_def Rep_PDUnit by simp 28 29lemma PDUnit_convex_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<natural> PDUnit y" 30unfolding convex_le_def by (fast intro: PDUnit_upper_mono PDUnit_lower_mono) 31 32lemma PDPlus_convex_mono: "\<lbrakk>s \<le>\<natural> t; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<natural> PDPlus t v" 33unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono) 34 35lemma convex_le_PDUnit_PDUnit_iff [simp]: 36 "(PDUnit a \<le>\<natural> PDUnit b) = (a \<sqsubseteq> b)" 37unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast 38 39lemma convex_le_PDUnit_lemma1: 40 "(PDUnit a \<le>\<natural> t) = (\<forall>b\<in>Rep_pd_basis t. a \<sqsubseteq> b)" 41unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit 42using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast 43 44lemma convex_le_PDUnit_PDPlus_iff [simp]: 45 "(PDUnit a \<le>\<natural> PDPlus t u) = (PDUnit a \<le>\<natural> t \<and> PDUnit a \<le>\<natural> u)" 46unfolding convex_le_PDUnit_lemma1 Rep_PDPlus by fast 47 48lemma convex_le_PDUnit_lemma2: 49 "(t \<le>\<natural> PDUnit b) = (\<forall>a\<in>Rep_pd_basis t. a \<sqsubseteq> b)" 50unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit 51using Rep_pd_basis_nonempty [of t, folded ex_in_conv] by fast 52 53lemma convex_le_PDPlus_PDUnit_iff [simp]: 54 "(PDPlus t u \<le>\<natural> PDUnit a) = (t \<le>\<natural> PDUnit a \<and> u \<le>\<natural> PDUnit a)" 55unfolding convex_le_PDUnit_lemma2 Rep_PDPlus by fast 56 57lemma convex_le_PDPlus_lemma: 58 assumes z: "PDPlus t u \<le>\<natural> z" 59 shows "\<exists>v w. z = PDPlus v w \<and> t \<le>\<natural> v \<and> u \<le>\<natural> w" 60proof (intro exI conjI) 61 let ?A = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis t. a \<sqsubseteq> b}" 62 let ?B = "{b\<in>Rep_pd_basis z. \<exists>a\<in>Rep_pd_basis u. a \<sqsubseteq> b}" 63 let ?v = "Abs_pd_basis ?A" 64 let ?w = "Abs_pd_basis ?B" 65 have Rep_v: "Rep_pd_basis ?v = ?A" 66 apply (rule Abs_pd_basis_inverse) 67 apply (rule Rep_pd_basis_nonempty [of t, folded ex_in_conv, THEN exE]) 68 apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify) 69 apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE) 70 apply (simp add: pd_basis_def) 71 apply fast 72 done 73 have Rep_w: "Rep_pd_basis ?w = ?B" 74 apply (rule Abs_pd_basis_inverse) 75 apply (rule Rep_pd_basis_nonempty [of u, folded ex_in_conv, THEN exE]) 76 apply (cut_tac z, simp only: convex_le_def lower_le_def, clarify) 77 apply (drule_tac x=x in bspec, simp add: Rep_PDPlus, erule bexE) 78 apply (simp add: pd_basis_def) 79 apply fast 80 done 81 show "z = PDPlus ?v ?w" 82 apply (insert z) 83 apply (simp add: convex_le_def, erule conjE) 84 apply (simp add: Rep_pd_basis_inject [symmetric] Rep_PDPlus) 85 apply (simp add: Rep_v Rep_w) 86 apply (rule equalityI) 87 apply (rule subsetI) 88 apply (simp only: upper_le_def) 89 apply (drule (1) bspec, erule bexE) 90 apply (simp add: Rep_PDPlus) 91 apply fast 92 apply fast 93 done 94 show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w" 95 apply (insert z) 96 apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w) 97 apply fast+ 98 done 99qed 100 101lemma convex_le_induct [induct set: convex_le]: 102 assumes le: "t \<le>\<natural> u" 103 assumes 2: "\<And>t u v. \<lbrakk>P t u; P u v\<rbrakk> \<Longrightarrow> P t v" 104 assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)" 105 assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)" 106 shows "P t u" 107using le apply (induct t arbitrary: u rule: pd_basis_induct) 108apply (erule rev_mp) 109apply (induct_tac u rule: pd_basis_induct1) 110apply (simp add: 3) 111apply (simp, clarify, rename_tac a b t) 112apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)") 113apply (simp add: PDPlus_absorb) 114apply (erule (1) 4 [OF 3]) 115apply (drule convex_le_PDPlus_lemma, clarify) 116apply (simp add: 4) 117done 118 119 120subsection \<open>Type definition\<close> 121 122typedef 'a convex_pd ("('(_')\<natural>)") = 123 "{S::'a pd_basis set. convex_le.ideal S}" 124by (rule convex_le.ex_ideal) 125 126instantiation convex_pd :: (bifinite) below 127begin 128 129definition 130 "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y" 131 132instance .. 133end 134 135instance convex_pd :: (bifinite) po 136using type_definition_convex_pd below_convex_pd_def 137by (rule convex_le.typedef_ideal_po) 138 139instance convex_pd :: (bifinite) cpo 140using type_definition_convex_pd below_convex_pd_def 141by (rule convex_le.typedef_ideal_cpo) 142 143definition 144 convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where 145 "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}" 146 147interpretation convex_pd: 148 ideal_completion convex_le convex_principal Rep_convex_pd 149using type_definition_convex_pd below_convex_pd_def 150using convex_principal_def pd_basis_countable 151by (rule convex_le.typedef_ideal_completion) 152 153text \<open>Convex powerdomain is pointed\<close> 154 155lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys" 156by (induct ys rule: convex_pd.principal_induct, simp, simp) 157 158instance convex_pd :: (bifinite) pcpo 159by intro_classes (fast intro: convex_pd_minimal) 160 161lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)" 162by (rule convex_pd_minimal [THEN bottomI, symmetric]) 163 164 165subsection \<open>Monadic unit and plus\<close> 166 167definition 168 convex_unit :: "'a \<rightarrow> 'a convex_pd" where 169 "convex_unit = compact_basis.extension (\<lambda>a. convex_principal (PDUnit a))" 170 171definition 172 convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where 173 "convex_plus = convex_pd.extension (\<lambda>t. convex_pd.extension (\<lambda>u. 174 convex_principal (PDPlus t u)))" 175 176abbreviation 177 convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd" 178 (infixl "\<union>\<natural>" 65) where 179 "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" 180 181syntax 182 "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>") 183 184translations 185 "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>" 186 "{x}\<natural>" == "CONST convex_unit\<cdot>x" 187 188lemma convex_unit_Rep_compact_basis [simp]: 189 "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)" 190unfolding convex_unit_def 191by (simp add: compact_basis.extension_principal PDUnit_convex_mono) 192 193lemma convex_plus_principal [simp]: 194 "convex_principal t \<union>\<natural> convex_principal u = convex_principal (PDPlus t u)" 195unfolding convex_plus_def 196by (simp add: convex_pd.extension_principal 197 convex_pd.extension_mono PDPlus_convex_mono) 198 199interpretation convex_add: semilattice convex_add proof 200 fix xs ys zs :: "'a convex_pd" 201 show "(xs \<union>\<natural> ys) \<union>\<natural> zs = xs \<union>\<natural> (ys \<union>\<natural> zs)" 202 apply (induct xs rule: convex_pd.principal_induct, simp) 203 apply (induct ys rule: convex_pd.principal_induct, simp) 204 apply (induct zs rule: convex_pd.principal_induct, simp) 205 apply (simp add: PDPlus_assoc) 206 done 207 show "xs \<union>\<natural> ys = ys \<union>\<natural> xs" 208 apply (induct xs rule: convex_pd.principal_induct, simp) 209 apply (induct ys rule: convex_pd.principal_induct, simp) 210 apply (simp add: PDPlus_commute) 211 done 212 show "xs \<union>\<natural> xs = xs" 213 apply (induct xs rule: convex_pd.principal_induct, simp) 214 apply (simp add: PDPlus_absorb) 215 done 216qed 217 218lemmas convex_plus_assoc = convex_add.assoc 219lemmas convex_plus_commute = convex_add.commute 220lemmas convex_plus_absorb = convex_add.idem 221lemmas convex_plus_left_commute = convex_add.left_commute 222lemmas convex_plus_left_absorb = convex_add.left_idem 223 224text \<open>Useful for \<open>simp add: convex_plus_ac\<close>\<close> 225lemmas convex_plus_ac = 226 convex_plus_assoc convex_plus_commute convex_plus_left_commute 227 228text \<open>Useful for \<open>simp only: convex_plus_aci\<close>\<close> 229lemmas convex_plus_aci = 230 convex_plus_ac convex_plus_absorb convex_plus_left_absorb 231 232lemma convex_unit_below_plus_iff [simp]: 233 "{x}\<natural> \<sqsubseteq> ys \<union>\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs" 234apply (induct x rule: compact_basis.principal_induct, simp) 235apply (induct ys rule: convex_pd.principal_induct, simp) 236apply (induct zs rule: convex_pd.principal_induct, simp) 237apply simp 238done 239 240lemma convex_plus_below_unit_iff [simp]: 241 "xs \<union>\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>" 242apply (induct xs rule: convex_pd.principal_induct, simp) 243apply (induct ys rule: convex_pd.principal_induct, simp) 244apply (induct z rule: compact_basis.principal_induct, simp) 245apply simp 246done 247 248lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y" 249apply (induct x rule: compact_basis.principal_induct, simp) 250apply (induct y rule: compact_basis.principal_induct, simp) 251apply simp 252done 253 254lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y" 255unfolding po_eq_conv by simp 256 257lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>" 258using convex_unit_Rep_compact_basis [of compact_bot] 259by (simp add: inst_convex_pd_pcpo) 260 261lemma convex_unit_bottom_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>" 262unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff) 263 264lemma compact_convex_unit: "compact x \<Longrightarrow> compact {x}\<natural>" 265by (auto dest!: compact_basis.compact_imp_principal) 266 267lemma compact_convex_unit_iff [simp]: "compact {x}\<natural> \<longleftrightarrow> compact x" 268apply (safe elim!: compact_convex_unit) 269apply (simp only: compact_def convex_unit_below_iff [symmetric]) 270apply (erule adm_subst [OF cont_Rep_cfun2]) 271done 272 273lemma compact_convex_plus [simp]: 274 "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<natural> ys)" 275by (auto dest!: convex_pd.compact_imp_principal) 276 277 278subsection \<open>Induction rules\<close> 279 280lemma convex_pd_induct1: 281 assumes P: "adm P" 282 assumes unit: "\<And>x. P {x}\<natural>" 283 assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)" 284 shows "P (xs::'a convex_pd)" 285apply (induct xs rule: convex_pd.principal_induct, rule P) 286apply (induct_tac a rule: pd_basis_induct1) 287apply (simp only: convex_unit_Rep_compact_basis [symmetric]) 288apply (rule unit) 289apply (simp only: convex_unit_Rep_compact_basis [symmetric] 290 convex_plus_principal [symmetric]) 291apply (erule insert [OF unit]) 292done 293 294lemma convex_pd_induct 295 [case_names adm convex_unit convex_plus, induct type: convex_pd]: 296 assumes P: "adm P" 297 assumes unit: "\<And>x. P {x}\<natural>" 298 assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)" 299 shows "P (xs::'a convex_pd)" 300apply (induct xs rule: convex_pd.principal_induct, rule P) 301apply (induct_tac a rule: pd_basis_induct) 302apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit) 303apply (simp only: convex_plus_principal [symmetric] plus) 304done 305 306 307subsection \<open>Monadic bind\<close> 308 309definition 310 convex_bind_basis :: 311 "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where 312 "convex_bind_basis = fold_pd 313 (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a)) 314 (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" 315 316lemma ACI_convex_bind: 317 "semilattice (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" 318apply unfold_locales 319apply (simp add: convex_plus_assoc) 320apply (simp add: convex_plus_commute) 321apply (simp add: eta_cfun) 322done 323 324lemma convex_bind_basis_simps [simp]: 325 "convex_bind_basis (PDUnit a) = 326 (\<Lambda> f. f\<cdot>(Rep_compact_basis a))" 327 "convex_bind_basis (PDPlus t u) = 328 (\<Lambda> f. convex_bind_basis t\<cdot>f \<union>\<natural> convex_bind_basis u\<cdot>f)" 329unfolding convex_bind_basis_def 330apply - 331apply (rule fold_pd_PDUnit [OF ACI_convex_bind]) 332apply (rule fold_pd_PDPlus [OF ACI_convex_bind]) 333done 334 335lemma convex_bind_basis_mono: 336 "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u" 337apply (erule convex_le_induct) 338apply (erule (1) below_trans) 339apply (simp add: monofun_LAM monofun_cfun) 340apply (simp add: monofun_LAM monofun_cfun) 341done 342 343definition 344 convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where 345 "convex_bind = convex_pd.extension convex_bind_basis" 346 347syntax 348 "_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic" 349 ("(3\<Union>\<natural>_\<in>_./ _)" [0, 0, 10] 10) 350 351translations 352 "\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)" 353 354lemma convex_bind_principal [simp]: 355 "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t" 356unfolding convex_bind_def 357apply (rule convex_pd.extension_principal) 358apply (erule convex_bind_basis_mono) 359done 360 361lemma convex_bind_unit [simp]: 362 "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x" 363by (induct x rule: compact_basis.principal_induct, simp, simp) 364 365lemma convex_bind_plus [simp]: 366 "convex_bind\<cdot>(xs \<union>\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f \<union>\<natural> convex_bind\<cdot>ys\<cdot>f" 367by (induct xs rule: convex_pd.principal_induct, simp, 368 induct ys rule: convex_pd.principal_induct, simp, simp) 369 370lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" 371unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit) 372 373lemma convex_bind_bind: 374 "convex_bind\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>g = 375 convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_bind\<cdot>(f\<cdot>x)\<cdot>g)" 376by (induct xs, simp_all) 377 378 379subsection \<open>Map\<close> 380 381definition 382 convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where 383 "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))" 384 385lemma convex_map_unit [simp]: 386 "convex_map\<cdot>f\<cdot>{x}\<natural> = {f\<cdot>x}\<natural>" 387unfolding convex_map_def by simp 388 389lemma convex_map_plus [simp]: 390 "convex_map\<cdot>f\<cdot>(xs \<union>\<natural> ys) = convex_map\<cdot>f\<cdot>xs \<union>\<natural> convex_map\<cdot>f\<cdot>ys" 391unfolding convex_map_def by simp 392 393lemma convex_map_bottom [simp]: "convex_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<natural>" 394unfolding convex_map_def by simp 395 396lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 397by (induct xs rule: convex_pd_induct, simp_all) 398 399lemma convex_map_ID: "convex_map\<cdot>ID = ID" 400by (simp add: cfun_eq_iff ID_def convex_map_ident) 401 402lemma convex_map_map: 403 "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" 404by (induct xs rule: convex_pd_induct, simp_all) 405 406lemma convex_bind_map: 407 "convex_bind\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>g = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))" 408by (simp add: convex_map_def convex_bind_bind) 409 410lemma convex_map_bind: 411 "convex_map\<cdot>f\<cdot>(convex_bind\<cdot>xs\<cdot>g) = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_map\<cdot>f\<cdot>(g\<cdot>x))" 412by (simp add: convex_map_def convex_bind_bind) 413 414lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)" 415apply standard 416apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) 417apply (induct_tac y rule: convex_pd_induct) 418apply (simp_all add: ep_pair.e_p_below monofun_cfun) 419done 420 421lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)" 422apply standard 423apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) 424apply (induct_tac x rule: convex_pd_induct) 425apply (simp_all add: deflation.below monofun_cfun) 426done 427 428(* FIXME: long proof! *) 429lemma finite_deflation_convex_map: 430 assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)" 431proof (rule finite_deflation_intro) 432 interpret d: finite_deflation d by fact 433 from d.deflation_axioms show "deflation (convex_map\<cdot>d)" 434 by (rule deflation_convex_map) 435 have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range) 436 hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))" 437 by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) 438 hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp 439 hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" 440 by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) 441 hence *: "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp 442 hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))" 443 apply (rule rev_finite_subset) 444 apply clarsimp 445 apply (induct_tac xs rule: convex_pd.principal_induct) 446 apply (simp add: adm_mem_finite *) 447 apply (rename_tac t, induct_tac t rule: pd_basis_induct) 448 apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit) 449 apply simp 450 apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b") 451 apply clarsimp 452 apply (rule imageI) 453 apply (rule vimageI2) 454 apply (simp add: Rep_PDUnit) 455 apply (rule range_eqI) 456 apply (erule sym) 457 apply (rule exI) 458 apply (rule Abs_compact_basis_inverse [symmetric]) 459 apply (simp add: d.compact) 460 apply (simp only: convex_plus_principal [symmetric] convex_map_plus) 461 apply clarsimp 462 apply (rule imageI) 463 apply (rule vimageI2) 464 apply (simp add: Rep_PDPlus) 465 done 466 thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}" 467 by (rule finite_range_imp_finite_fixes) 468qed 469 470subsection \<open>Convex powerdomain is bifinite\<close> 471 472lemma approx_chain_convex_map: 473 assumes "approx_chain a" 474 shows "approx_chain (\<lambda>i. convex_map\<cdot>(a i))" 475 using assms unfolding approx_chain_def 476 by (simp add: lub_APP convex_map_ID finite_deflation_convex_map) 477 478instance convex_pd :: (bifinite) bifinite 479proof 480 show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a" 481 using bifinite [where 'a='a] 482 by (fast intro!: approx_chain_convex_map) 483qed 484 485subsection \<open>Join\<close> 486 487definition 488 convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where 489 "convex_join = (\<Lambda> xss. convex_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 490 491lemma convex_join_unit [simp]: 492 "convex_join\<cdot>{xs}\<natural> = xs" 493unfolding convex_join_def by simp 494 495lemma convex_join_plus [simp]: 496 "convex_join\<cdot>(xss \<union>\<natural> yss) = convex_join\<cdot>xss \<union>\<natural> convex_join\<cdot>yss" 497unfolding convex_join_def by simp 498 499lemma convex_join_bottom [simp]: "convex_join\<cdot>\<bottom> = \<bottom>" 500unfolding convex_join_def by simp 501 502lemma convex_join_map_unit: 503 "convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs" 504by (induct xs rule: convex_pd_induct, simp_all) 505 506lemma convex_join_map_join: 507 "convex_join\<cdot>(convex_map\<cdot>convex_join\<cdot>xsss) = convex_join\<cdot>(convex_join\<cdot>xsss)" 508by (induct xsss rule: convex_pd_induct, simp_all) 509 510lemma convex_join_map_map: 511 "convex_join\<cdot>(convex_map\<cdot>(convex_map\<cdot>f)\<cdot>xss) = 512 convex_map\<cdot>f\<cdot>(convex_join\<cdot>xss)" 513by (induct xss rule: convex_pd_induct, simp_all) 514 515 516subsection \<open>Conversions to other powerdomains\<close> 517 518text \<open>Convex to upper\<close> 519 520lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u" 521unfolding convex_le_def by simp 522 523definition 524 convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where 525 "convex_to_upper = convex_pd.extension upper_principal" 526 527lemma convex_to_upper_principal [simp]: 528 "convex_to_upper\<cdot>(convex_principal t) = upper_principal t" 529unfolding convex_to_upper_def 530apply (rule convex_pd.extension_principal) 531apply (rule upper_pd.principal_mono) 532apply (erule convex_le_imp_upper_le) 533done 534 535lemma convex_to_upper_unit [simp]: 536 "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>" 537by (induct x rule: compact_basis.principal_induct, simp, simp) 538 539lemma convex_to_upper_plus [simp]: 540 "convex_to_upper\<cdot>(xs \<union>\<natural> ys) = convex_to_upper\<cdot>xs \<union>\<sharp> convex_to_upper\<cdot>ys" 541by (induct xs rule: convex_pd.principal_induct, simp, 542 induct ys rule: convex_pd.principal_induct, simp, simp) 543 544lemma convex_to_upper_bind [simp]: 545 "convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) = 546 upper_bind\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper oo f)" 547by (induct xs rule: convex_pd_induct, simp, simp, simp) 548 549lemma convex_to_upper_map [simp]: 550 "convex_to_upper\<cdot>(convex_map\<cdot>f\<cdot>xs) = upper_map\<cdot>f\<cdot>(convex_to_upper\<cdot>xs)" 551by (simp add: convex_map_def upper_map_def cfcomp_LAM) 552 553lemma convex_to_upper_join [simp]: 554 "convex_to_upper\<cdot>(convex_join\<cdot>xss) = 555 upper_bind\<cdot>(convex_to_upper\<cdot>xss)\<cdot>convex_to_upper" 556by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun) 557 558text \<open>Convex to lower\<close> 559 560lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u" 561unfolding convex_le_def by simp 562 563definition 564 convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where 565 "convex_to_lower = convex_pd.extension lower_principal" 566 567lemma convex_to_lower_principal [simp]: 568 "convex_to_lower\<cdot>(convex_principal t) = lower_principal t" 569unfolding convex_to_lower_def 570apply (rule convex_pd.extension_principal) 571apply (rule lower_pd.principal_mono) 572apply (erule convex_le_imp_lower_le) 573done 574 575lemma convex_to_lower_unit [simp]: 576 "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>" 577by (induct x rule: compact_basis.principal_induct, simp, simp) 578 579lemma convex_to_lower_plus [simp]: 580 "convex_to_lower\<cdot>(xs \<union>\<natural> ys) = convex_to_lower\<cdot>xs \<union>\<flat> convex_to_lower\<cdot>ys" 581by (induct xs rule: convex_pd.principal_induct, simp, 582 induct ys rule: convex_pd.principal_induct, simp, simp) 583 584lemma convex_to_lower_bind [simp]: 585 "convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) = 586 lower_bind\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower oo f)" 587by (induct xs rule: convex_pd_induct, simp, simp, simp) 588 589lemma convex_to_lower_map [simp]: 590 "convex_to_lower\<cdot>(convex_map\<cdot>f\<cdot>xs) = lower_map\<cdot>f\<cdot>(convex_to_lower\<cdot>xs)" 591by (simp add: convex_map_def lower_map_def cfcomp_LAM) 592 593lemma convex_to_lower_join [simp]: 594 "convex_to_lower\<cdot>(convex_join\<cdot>xss) = 595 lower_bind\<cdot>(convex_to_lower\<cdot>xss)\<cdot>convex_to_lower" 596by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun) 597 598text \<open>Ordering property\<close> 599 600lemma convex_pd_below_iff: 601 "(xs \<sqsubseteq> ys) = 602 (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and> 603 convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)" 604apply (induct xs rule: convex_pd.principal_induct, simp) 605apply (induct ys rule: convex_pd.principal_induct, simp) 606apply (simp add: convex_le_def) 607done 608 609lemmas convex_plus_below_plus_iff = 610 convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws"] 611 for xs ys zs ws 612 613lemmas convex_pd_below_simps = 614 convex_unit_below_plus_iff 615 convex_plus_below_unit_iff 616 convex_plus_below_plus_iff 617 convex_unit_below_iff 618 convex_to_upper_unit 619 convex_to_upper_plus 620 convex_to_lower_unit 621 convex_to_lower_plus 622 upper_pd_below_simps 623 lower_pd_below_simps 624 625end 626