1(* Title: HOL/HOLCF/UpperPD.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Upper powerdomain\<close> 6 7theory UpperPD 8imports Compact_Basis 9begin 10 11subsection \<open>Basis preorder\<close> 12 13definition 14 upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where 15 "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)" 16 17lemma upper_le_refl [simp]: "t \<le>\<sharp> t" 18unfolding upper_le_def by fast 19 20lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v" 21unfolding upper_le_def 22apply (rule ballI) 23apply (drule (1) bspec, erule bexE) 24apply (drule (1) bspec, erule bexE) 25apply (erule rev_bexI) 26apply (erule (1) below_trans) 27done 28 29interpretation upper_le: preorder upper_le 30by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans) 31 32lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t" 33unfolding upper_le_def Rep_PDUnit by simp 34 35lemma PDUnit_upper_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y" 36unfolding upper_le_def Rep_PDUnit by simp 37 38lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v" 39unfolding upper_le_def Rep_PDPlus by fast 40 41lemma PDPlus_upper_le: "PDPlus t u \<le>\<sharp> t" 42unfolding upper_le_def Rep_PDPlus by fast 43 44lemma upper_le_PDUnit_PDUnit_iff [simp]: 45 "(PDUnit a \<le>\<sharp> PDUnit b) = (a \<sqsubseteq> b)" 46unfolding upper_le_def Rep_PDUnit by fast 47 48lemma upper_le_PDPlus_PDUnit_iff: 49 "(PDPlus t u \<le>\<sharp> PDUnit a) = (t \<le>\<sharp> PDUnit a \<or> u \<le>\<sharp> PDUnit a)" 50unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast 51 52lemma upper_le_PDPlus_iff: "(t \<le>\<sharp> PDPlus u v) = (t \<le>\<sharp> u \<and> t \<le>\<sharp> v)" 53unfolding upper_le_def Rep_PDPlus by fast 54 55lemma upper_le_induct [induct set: upper_le]: 56 assumes le: "t \<le>\<sharp> u" 57 assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)" 58 assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)" 59 assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)" 60 shows "P t u" 61using le apply (induct u arbitrary: t rule: pd_basis_induct) 62apply (erule rev_mp) 63apply (induct_tac t rule: pd_basis_induct) 64apply (simp add: 1) 65apply (simp add: upper_le_PDPlus_PDUnit_iff) 66apply (simp add: 2) 67apply (subst PDPlus_commute) 68apply (simp add: 2) 69apply (simp add: upper_le_PDPlus_iff 3) 70done 71 72 73subsection \<open>Type definition\<close> 74 75typedef 'a upper_pd ("('(_')\<sharp>)") = 76 "{S::'a pd_basis set. upper_le.ideal S}" 77by (rule upper_le.ex_ideal) 78 79instantiation upper_pd :: (bifinite) below 80begin 81 82definition 83 "x \<sqsubseteq> y \<longleftrightarrow> Rep_upper_pd x \<subseteq> Rep_upper_pd y" 84 85instance .. 86end 87 88instance upper_pd :: (bifinite) po 89using type_definition_upper_pd below_upper_pd_def 90by (rule upper_le.typedef_ideal_po) 91 92instance upper_pd :: (bifinite) cpo 93using type_definition_upper_pd below_upper_pd_def 94by (rule upper_le.typedef_ideal_cpo) 95 96definition 97 upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where 98 "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}" 99 100interpretation upper_pd: 101 ideal_completion upper_le upper_principal Rep_upper_pd 102using type_definition_upper_pd below_upper_pd_def 103using upper_principal_def pd_basis_countable 104by (rule upper_le.typedef_ideal_completion) 105 106text \<open>Upper powerdomain is pointed\<close> 107 108lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys" 109by (induct ys rule: upper_pd.principal_induct, simp, simp) 110 111instance upper_pd :: (bifinite) pcpo 112by intro_classes (fast intro: upper_pd_minimal) 113 114lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)" 115by (rule upper_pd_minimal [THEN bottomI, symmetric]) 116 117 118subsection \<open>Monadic unit and plus\<close> 119 120definition 121 upper_unit :: "'a \<rightarrow> 'a upper_pd" where 122 "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))" 123 124definition 125 upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where 126 "upper_plus = upper_pd.extension (\<lambda>t. upper_pd.extension (\<lambda>u. 127 upper_principal (PDPlus t u)))" 128 129abbreviation 130 upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd" 131 (infixl "\<union>\<sharp>" 65) where 132 "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys" 133 134syntax 135 "_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>") 136 137translations 138 "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>" 139 "{x}\<sharp>" == "CONST upper_unit\<cdot>x" 140 141lemma upper_unit_Rep_compact_basis [simp]: 142 "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)" 143unfolding upper_unit_def 144by (simp add: compact_basis.extension_principal PDUnit_upper_mono) 145 146lemma upper_plus_principal [simp]: 147 "upper_principal t \<union>\<sharp> upper_principal u = upper_principal (PDPlus t u)" 148unfolding upper_plus_def 149by (simp add: upper_pd.extension_principal 150 upper_pd.extension_mono PDPlus_upper_mono) 151 152interpretation upper_add: semilattice upper_add proof 153 fix xs ys zs :: "'a upper_pd" 154 show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)" 155 apply (induct xs rule: upper_pd.principal_induct, simp) 156 apply (induct ys rule: upper_pd.principal_induct, simp) 157 apply (induct zs rule: upper_pd.principal_induct, simp) 158 apply (simp add: PDPlus_assoc) 159 done 160 show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs" 161 apply (induct xs rule: upper_pd.principal_induct, simp) 162 apply (induct ys rule: upper_pd.principal_induct, simp) 163 apply (simp add: PDPlus_commute) 164 done 165 show "xs \<union>\<sharp> xs = xs" 166 apply (induct xs rule: upper_pd.principal_induct, simp) 167 apply (simp add: PDPlus_absorb) 168 done 169qed 170 171lemmas upper_plus_assoc = upper_add.assoc 172lemmas upper_plus_commute = upper_add.commute 173lemmas upper_plus_absorb = upper_add.idem 174lemmas upper_plus_left_commute = upper_add.left_commute 175lemmas upper_plus_left_absorb = upper_add.left_idem 176 177text \<open>Useful for \<open>simp add: upper_plus_ac\<close>\<close> 178lemmas upper_plus_ac = 179 upper_plus_assoc upper_plus_commute upper_plus_left_commute 180 181text \<open>Useful for \<open>simp only: upper_plus_aci\<close>\<close> 182lemmas upper_plus_aci = 183 upper_plus_ac upper_plus_absorb upper_plus_left_absorb 184 185lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs" 186apply (induct xs rule: upper_pd.principal_induct, simp) 187apply (induct ys rule: upper_pd.principal_induct, simp) 188apply (simp add: PDPlus_upper_le) 189done 190 191lemma upper_plus_below2: "xs \<union>\<sharp> ys \<sqsubseteq> ys" 192by (subst upper_plus_commute, rule upper_plus_below1) 193 194lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys \<union>\<sharp> zs" 195apply (subst upper_plus_absorb [of xs, symmetric]) 196apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 197done 198 199lemma upper_below_plus_iff [simp]: 200 "xs \<sqsubseteq> ys \<union>\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs" 201apply safe 202apply (erule below_trans [OF _ upper_plus_below1]) 203apply (erule below_trans [OF _ upper_plus_below2]) 204apply (erule (1) upper_plus_greatest) 205done 206 207lemma upper_plus_below_unit_iff [simp]: 208 "xs \<union>\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>" 209apply (induct xs rule: upper_pd.principal_induct, simp) 210apply (induct ys rule: upper_pd.principal_induct, simp) 211apply (induct z rule: compact_basis.principal_induct, simp) 212apply (simp add: upper_le_PDPlus_PDUnit_iff) 213done 214 215lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y" 216apply (induct x rule: compact_basis.principal_induct, simp) 217apply (induct y rule: compact_basis.principal_induct, simp) 218apply simp 219done 220 221lemmas upper_pd_below_simps = 222 upper_unit_below_iff 223 upper_below_plus_iff 224 upper_plus_below_unit_iff 225 226lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y" 227unfolding po_eq_conv by simp 228 229lemma upper_unit_strict [simp]: "{\<bottom>}\<sharp> = \<bottom>" 230using upper_unit_Rep_compact_basis [of compact_bot] 231by (simp add: inst_upper_pd_pcpo) 232 233lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>" 234by (rule bottomI, rule upper_plus_below1) 235 236lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>" 237by (rule bottomI, rule upper_plus_below2) 238 239lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>" 240unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff) 241 242lemma upper_plus_bottom_iff [simp]: 243 "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>" 244apply (induct xs rule: upper_pd.principal_induct, simp) 245apply (induct ys rule: upper_pd.principal_induct, simp) 246apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff 247 upper_le_PDPlus_PDUnit_iff) 248done 249 250lemma compact_upper_unit: "compact x \<Longrightarrow> compact {x}\<sharp>" 251by (auto dest!: compact_basis.compact_imp_principal) 252 253lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x" 254apply (safe elim!: compact_upper_unit) 255apply (simp only: compact_def upper_unit_below_iff [symmetric]) 256apply (erule adm_subst [OF cont_Rep_cfun2]) 257done 258 259lemma compact_upper_plus [simp]: 260 "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)" 261by (auto dest!: upper_pd.compact_imp_principal) 262 263 264subsection \<open>Induction rules\<close> 265 266lemma upper_pd_induct1: 267 assumes P: "adm P" 268 assumes unit: "\<And>x. P {x}\<sharp>" 269 assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)" 270 shows "P (xs::'a upper_pd)" 271apply (induct xs rule: upper_pd.principal_induct, rule P) 272apply (induct_tac a rule: pd_basis_induct1) 273apply (simp only: upper_unit_Rep_compact_basis [symmetric]) 274apply (rule unit) 275apply (simp only: upper_unit_Rep_compact_basis [symmetric] 276 upper_plus_principal [symmetric]) 277apply (erule insert [OF unit]) 278done 279 280lemma upper_pd_induct 281 [case_names adm upper_unit upper_plus, induct type: upper_pd]: 282 assumes P: "adm P" 283 assumes unit: "\<And>x. P {x}\<sharp>" 284 assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)" 285 shows "P (xs::'a upper_pd)" 286apply (induct xs rule: upper_pd.principal_induct, rule P) 287apply (induct_tac a rule: pd_basis_induct) 288apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit) 289apply (simp only: upper_plus_principal [symmetric] plus) 290done 291 292 293subsection \<open>Monadic bind\<close> 294 295definition 296 upper_bind_basis :: 297 "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where 298 "upper_bind_basis = fold_pd 299 (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a)) 300 (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)" 301 302lemma ACI_upper_bind: 303 "semilattice (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)" 304apply unfold_locales 305apply (simp add: upper_plus_assoc) 306apply (simp add: upper_plus_commute) 307apply (simp add: eta_cfun) 308done 309 310lemma upper_bind_basis_simps [simp]: 311 "upper_bind_basis (PDUnit a) = 312 (\<Lambda> f. f\<cdot>(Rep_compact_basis a))" 313 "upper_bind_basis (PDPlus t u) = 314 (\<Lambda> f. upper_bind_basis t\<cdot>f \<union>\<sharp> upper_bind_basis u\<cdot>f)" 315unfolding upper_bind_basis_def 316apply - 317apply (rule fold_pd_PDUnit [OF ACI_upper_bind]) 318apply (rule fold_pd_PDPlus [OF ACI_upper_bind]) 319done 320 321lemma upper_bind_basis_mono: 322 "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u" 323unfolding cfun_below_iff 324apply (erule upper_le_induct, safe) 325apply (simp add: monofun_cfun) 326apply (simp add: below_trans [OF upper_plus_below1]) 327apply simp 328done 329 330definition 331 upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where 332 "upper_bind = upper_pd.extension upper_bind_basis" 333 334syntax 335 "_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic" 336 ("(3\<Union>\<sharp>_\<in>_./ _)" [0, 0, 10] 10) 337 338translations 339 "\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)" 340 341lemma upper_bind_principal [simp]: 342 "upper_bind\<cdot>(upper_principal t) = upper_bind_basis t" 343unfolding upper_bind_def 344apply (rule upper_pd.extension_principal) 345apply (erule upper_bind_basis_mono) 346done 347 348lemma upper_bind_unit [simp]: 349 "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x" 350by (induct x rule: compact_basis.principal_induct, simp, simp) 351 352lemma upper_bind_plus [simp]: 353 "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f" 354by (induct xs rule: upper_pd.principal_induct, simp, 355 induct ys rule: upper_pd.principal_induct, simp, simp) 356 357lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" 358unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit) 359 360lemma upper_bind_bind: 361 "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)" 362by (induct xs, simp_all) 363 364 365subsection \<open>Map\<close> 366 367definition 368 upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where 369 "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))" 370 371lemma upper_map_unit [simp]: 372 "upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>" 373unfolding upper_map_def by simp 374 375lemma upper_map_plus [simp]: 376 "upper_map\<cdot>f\<cdot>(xs \<union>\<sharp> ys) = upper_map\<cdot>f\<cdot>xs \<union>\<sharp> upper_map\<cdot>f\<cdot>ys" 377unfolding upper_map_def by simp 378 379lemma upper_map_bottom [simp]: "upper_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<sharp>" 380unfolding upper_map_def by simp 381 382lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 383by (induct xs rule: upper_pd_induct, simp_all) 384 385lemma upper_map_ID: "upper_map\<cdot>ID = ID" 386by (simp add: cfun_eq_iff ID_def upper_map_ident) 387 388lemma upper_map_map: 389 "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" 390by (induct xs rule: upper_pd_induct, simp_all) 391 392lemma upper_bind_map: 393 "upper_bind\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))" 394by (simp add: upper_map_def upper_bind_bind) 395 396lemma upper_map_bind: 397 "upper_map\<cdot>f\<cdot>(upper_bind\<cdot>xs\<cdot>g) = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_map\<cdot>f\<cdot>(g\<cdot>x))" 398by (simp add: upper_map_def upper_bind_bind) 399 400lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)" 401apply standard 402apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse) 403apply (induct_tac y rule: upper_pd_induct) 404apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff) 405done 406 407lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)" 408apply standard 409apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem) 410apply (induct_tac x rule: upper_pd_induct) 411apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff) 412done 413 414(* FIXME: long proof! *) 415lemma finite_deflation_upper_map: 416 assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)" 417proof (rule finite_deflation_intro) 418 interpret d: finite_deflation d by fact 419 from d.deflation_axioms show "deflation (upper_map\<cdot>d)" 420 by (rule deflation_upper_map) 421 have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range) 422 hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))" 423 by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) 424 hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp 425 hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" 426 by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) 427 hence *: "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp 428 hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))" 429 apply (rule rev_finite_subset) 430 apply clarsimp 431 apply (induct_tac xs rule: upper_pd.principal_induct) 432 apply (simp add: adm_mem_finite *) 433 apply (rename_tac t, induct_tac t rule: pd_basis_induct) 434 apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit) 435 apply simp 436 apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b") 437 apply clarsimp 438 apply (rule imageI) 439 apply (rule vimageI2) 440 apply (simp add: Rep_PDUnit) 441 apply (rule range_eqI) 442 apply (erule sym) 443 apply (rule exI) 444 apply (rule Abs_compact_basis_inverse [symmetric]) 445 apply (simp add: d.compact) 446 apply (simp only: upper_plus_principal [symmetric] upper_map_plus) 447 apply clarsimp 448 apply (rule imageI) 449 apply (rule vimageI2) 450 apply (simp add: Rep_PDPlus) 451 done 452 thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}" 453 by (rule finite_range_imp_finite_fixes) 454qed 455 456subsection \<open>Upper powerdomain is bifinite\<close> 457 458lemma approx_chain_upper_map: 459 assumes "approx_chain a" 460 shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))" 461 using assms unfolding approx_chain_def 462 by (simp add: lub_APP upper_map_ID finite_deflation_upper_map) 463 464instance upper_pd :: (bifinite) bifinite 465proof 466 show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a" 467 using bifinite [where 'a='a] 468 by (fast intro!: approx_chain_upper_map) 469qed 470 471subsection \<open>Join\<close> 472 473definition 474 upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where 475 "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 476 477lemma upper_join_unit [simp]: 478 "upper_join\<cdot>{xs}\<sharp> = xs" 479unfolding upper_join_def by simp 480 481lemma upper_join_plus [simp]: 482 "upper_join\<cdot>(xss \<union>\<sharp> yss) = upper_join\<cdot>xss \<union>\<sharp> upper_join\<cdot>yss" 483unfolding upper_join_def by simp 484 485lemma upper_join_bottom [simp]: "upper_join\<cdot>\<bottom> = \<bottom>" 486unfolding upper_join_def by simp 487 488lemma upper_join_map_unit: 489 "upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs" 490by (induct xs rule: upper_pd_induct, simp_all) 491 492lemma upper_join_map_join: 493 "upper_join\<cdot>(upper_map\<cdot>upper_join\<cdot>xsss) = upper_join\<cdot>(upper_join\<cdot>xsss)" 494by (induct xsss rule: upper_pd_induct, simp_all) 495 496lemma upper_join_map_map: 497 "upper_join\<cdot>(upper_map\<cdot>(upper_map\<cdot>f)\<cdot>xss) = 498 upper_map\<cdot>f\<cdot>(upper_join\<cdot>xss)" 499by (induct xss rule: upper_pd_induct, simp_all) 500 501end 502