1(* Title: HOL/HOLCF/LowerPD.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Lower powerdomain\<close> 6 7theory LowerPD 8imports Compact_Basis 9begin 10 11subsection \<open>Basis preorder\<close> 12 13definition 14 lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<flat>" 50) where 15 "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. x \<sqsubseteq> y)" 16 17lemma lower_le_refl [simp]: "t \<le>\<flat> t" 18unfolding lower_le_def by fast 19 20lemma lower_le_trans: "\<lbrakk>t \<le>\<flat> u; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> t \<le>\<flat> v" 21unfolding lower_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 lower_le: preorder lower_le 30by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans) 31 32lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t" 33unfolding lower_le_def Rep_PDUnit 34by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv]) 35 36lemma PDUnit_lower_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y" 37unfolding lower_le_def Rep_PDUnit by fast 38 39lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v" 40unfolding lower_le_def Rep_PDPlus by fast 41 42lemma PDPlus_lower_le: "t \<le>\<flat> PDPlus t u" 43unfolding lower_le_def Rep_PDPlus by fast 44 45lemma lower_le_PDUnit_PDUnit_iff [simp]: 46 "(PDUnit a \<le>\<flat> PDUnit b) = (a \<sqsubseteq> b)" 47unfolding lower_le_def Rep_PDUnit by fast 48 49lemma lower_le_PDUnit_PDPlus_iff: 50 "(PDUnit a \<le>\<flat> PDPlus t u) = (PDUnit a \<le>\<flat> t \<or> PDUnit a \<le>\<flat> u)" 51unfolding lower_le_def Rep_PDPlus Rep_PDUnit by fast 52 53lemma lower_le_PDPlus_iff: "(PDPlus t u \<le>\<flat> v) = (t \<le>\<flat> v \<and> u \<le>\<flat> v)" 54unfolding lower_le_def Rep_PDPlus by fast 55 56lemma lower_le_induct [induct set: lower_le]: 57 assumes le: "t \<le>\<flat> u" 58 assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)" 59 assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)" 60 assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v" 61 shows "P t u" 62using le 63apply (induct t arbitrary: u rule: pd_basis_induct) 64apply (erule rev_mp) 65apply (induct_tac u rule: pd_basis_induct) 66apply (simp add: 1) 67apply (simp add: lower_le_PDUnit_PDPlus_iff) 68apply (simp add: 2) 69apply (subst PDPlus_commute) 70apply (simp add: 2) 71apply (simp add: lower_le_PDPlus_iff 3) 72done 73 74 75subsection \<open>Type definition\<close> 76 77typedef 'a lower_pd ("('(_')\<flat>)") = 78 "{S::'a pd_basis set. lower_le.ideal S}" 79by (rule lower_le.ex_ideal) 80 81instantiation lower_pd :: (bifinite) below 82begin 83 84definition 85 "x \<sqsubseteq> y \<longleftrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y" 86 87instance .. 88end 89 90instance lower_pd :: (bifinite) po 91using type_definition_lower_pd below_lower_pd_def 92by (rule lower_le.typedef_ideal_po) 93 94instance lower_pd :: (bifinite) cpo 95using type_definition_lower_pd below_lower_pd_def 96by (rule lower_le.typedef_ideal_cpo) 97 98definition 99 lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where 100 "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}" 101 102interpretation lower_pd: 103 ideal_completion lower_le lower_principal Rep_lower_pd 104using type_definition_lower_pd below_lower_pd_def 105using lower_principal_def pd_basis_countable 106by (rule lower_le.typedef_ideal_completion) 107 108text \<open>Lower powerdomain is pointed\<close> 109 110lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys" 111by (induct ys rule: lower_pd.principal_induct, simp, simp) 112 113instance lower_pd :: (bifinite) pcpo 114by intro_classes (fast intro: lower_pd_minimal) 115 116lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)" 117by (rule lower_pd_minimal [THEN bottomI, symmetric]) 118 119 120subsection \<open>Monadic unit and plus\<close> 121 122definition 123 lower_unit :: "'a \<rightarrow> 'a lower_pd" where 124 "lower_unit = compact_basis.extension (\<lambda>a. lower_principal (PDUnit a))" 125 126definition 127 lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where 128 "lower_plus = lower_pd.extension (\<lambda>t. lower_pd.extension (\<lambda>u. 129 lower_principal (PDPlus t u)))" 130 131abbreviation 132 lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd" 133 (infixl "\<union>\<flat>" 65) where 134 "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys" 135 136syntax 137 "_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>") 138 139translations 140 "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>" 141 "{x}\<flat>" == "CONST lower_unit\<cdot>x" 142 143lemma lower_unit_Rep_compact_basis [simp]: 144 "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)" 145unfolding lower_unit_def 146by (simp add: compact_basis.extension_principal PDUnit_lower_mono) 147 148lemma lower_plus_principal [simp]: 149 "lower_principal t \<union>\<flat> lower_principal u = lower_principal (PDPlus t u)" 150unfolding lower_plus_def 151by (simp add: lower_pd.extension_principal 152 lower_pd.extension_mono PDPlus_lower_mono) 153 154interpretation lower_add: semilattice lower_add proof 155 fix xs ys zs :: "'a lower_pd" 156 show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)" 157 apply (induct xs rule: lower_pd.principal_induct, simp) 158 apply (induct ys rule: lower_pd.principal_induct, simp) 159 apply (induct zs rule: lower_pd.principal_induct, simp) 160 apply (simp add: PDPlus_assoc) 161 done 162 show "xs \<union>\<flat> ys = ys \<union>\<flat> xs" 163 apply (induct xs rule: lower_pd.principal_induct, simp) 164 apply (induct ys rule: lower_pd.principal_induct, simp) 165 apply (simp add: PDPlus_commute) 166 done 167 show "xs \<union>\<flat> xs = xs" 168 apply (induct xs rule: lower_pd.principal_induct, simp) 169 apply (simp add: PDPlus_absorb) 170 done 171qed 172 173lemmas lower_plus_assoc = lower_add.assoc 174lemmas lower_plus_commute = lower_add.commute 175lemmas lower_plus_absorb = lower_add.idem 176lemmas lower_plus_left_commute = lower_add.left_commute 177lemmas lower_plus_left_absorb = lower_add.left_idem 178 179text \<open>Useful for \<open>simp add: lower_plus_ac\<close>\<close> 180lemmas lower_plus_ac = 181 lower_plus_assoc lower_plus_commute lower_plus_left_commute 182 183text \<open>Useful for \<open>simp only: lower_plus_aci\<close>\<close> 184lemmas lower_plus_aci = 185 lower_plus_ac lower_plus_absorb lower_plus_left_absorb 186 187lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys" 188apply (induct xs rule: lower_pd.principal_induct, simp) 189apply (induct ys rule: lower_pd.principal_induct, simp) 190apply (simp add: PDPlus_lower_le) 191done 192 193lemma lower_plus_below2: "ys \<sqsubseteq> xs \<union>\<flat> ys" 194by (subst lower_plus_commute, rule lower_plus_below1) 195 196lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<union>\<flat> ys \<sqsubseteq> zs" 197apply (subst lower_plus_absorb [of zs, symmetric]) 198apply (erule (1) monofun_cfun [OF monofun_cfun_arg]) 199done 200 201lemma lower_plus_below_iff [simp]: 202 "xs \<union>\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs" 203apply safe 204apply (erule below_trans [OF lower_plus_below1]) 205apply (erule below_trans [OF lower_plus_below2]) 206apply (erule (1) lower_plus_least) 207done 208 209lemma lower_unit_below_plus_iff [simp]: 210 "{x}\<flat> \<sqsubseteq> ys \<union>\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs" 211apply (induct x rule: compact_basis.principal_induct, simp) 212apply (induct ys rule: lower_pd.principal_induct, simp) 213apply (induct zs rule: lower_pd.principal_induct, simp) 214apply (simp add: lower_le_PDUnit_PDPlus_iff) 215done 216 217lemma lower_unit_below_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y" 218apply (induct x rule: compact_basis.principal_induct, simp) 219apply (induct y rule: compact_basis.principal_induct, simp) 220apply simp 221done 222 223lemmas lower_pd_below_simps = 224 lower_unit_below_iff 225 lower_plus_below_iff 226 lower_unit_below_plus_iff 227 228lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y" 229by (simp add: po_eq_conv) 230 231lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>" 232using lower_unit_Rep_compact_basis [of compact_bot] 233by (simp add: inst_lower_pd_pcpo) 234 235lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>" 236unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff) 237 238lemma lower_plus_bottom_iff [simp]: 239 "xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>" 240apply safe 241apply (rule bottomI, erule subst, rule lower_plus_below1) 242apply (rule bottomI, erule subst, rule lower_plus_below2) 243apply (rule lower_plus_absorb) 244done 245 246lemma lower_plus_strict1 [simp]: "\<bottom> \<union>\<flat> ys = ys" 247apply (rule below_antisym [OF _ lower_plus_below2]) 248apply (simp add: lower_plus_least) 249done 250 251lemma lower_plus_strict2 [simp]: "xs \<union>\<flat> \<bottom> = xs" 252apply (rule below_antisym [OF _ lower_plus_below1]) 253apply (simp add: lower_plus_least) 254done 255 256lemma compact_lower_unit: "compact x \<Longrightarrow> compact {x}\<flat>" 257by (auto dest!: compact_basis.compact_imp_principal) 258 259lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x" 260apply (safe elim!: compact_lower_unit) 261apply (simp only: compact_def lower_unit_below_iff [symmetric]) 262apply (erule adm_subst [OF cont_Rep_cfun2]) 263done 264 265lemma compact_lower_plus [simp]: 266 "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<flat> ys)" 267by (auto dest!: lower_pd.compact_imp_principal) 268 269 270subsection \<open>Induction rules\<close> 271 272lemma lower_pd_induct1: 273 assumes P: "adm P" 274 assumes unit: "\<And>x. P {x}\<flat>" 275 assumes insert: 276 "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)" 277 shows "P (xs::'a lower_pd)" 278apply (induct xs rule: lower_pd.principal_induct, rule P) 279apply (induct_tac a rule: pd_basis_induct1) 280apply (simp only: lower_unit_Rep_compact_basis [symmetric]) 281apply (rule unit) 282apply (simp only: lower_unit_Rep_compact_basis [symmetric] 283 lower_plus_principal [symmetric]) 284apply (erule insert [OF unit]) 285done 286 287lemma lower_pd_induct 288 [case_names adm lower_unit lower_plus, induct type: lower_pd]: 289 assumes P: "adm P" 290 assumes unit: "\<And>x. P {x}\<flat>" 291 assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)" 292 shows "P (xs::'a lower_pd)" 293apply (induct xs rule: lower_pd.principal_induct, rule P) 294apply (induct_tac a rule: pd_basis_induct) 295apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit) 296apply (simp only: lower_plus_principal [symmetric] plus) 297done 298 299 300subsection \<open>Monadic bind\<close> 301 302definition 303 lower_bind_basis :: 304 "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where 305 "lower_bind_basis = fold_pd 306 (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a)) 307 (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)" 308 309lemma ACI_lower_bind: 310 "semilattice (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)" 311apply unfold_locales 312apply (simp add: lower_plus_assoc) 313apply (simp add: lower_plus_commute) 314apply (simp add: eta_cfun) 315done 316 317lemma lower_bind_basis_simps [simp]: 318 "lower_bind_basis (PDUnit a) = 319 (\<Lambda> f. f\<cdot>(Rep_compact_basis a))" 320 "lower_bind_basis (PDPlus t u) = 321 (\<Lambda> f. lower_bind_basis t\<cdot>f \<union>\<flat> lower_bind_basis u\<cdot>f)" 322unfolding lower_bind_basis_def 323apply - 324apply (rule fold_pd_PDUnit [OF ACI_lower_bind]) 325apply (rule fold_pd_PDPlus [OF ACI_lower_bind]) 326done 327 328lemma lower_bind_basis_mono: 329 "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u" 330unfolding cfun_below_iff 331apply (erule lower_le_induct, safe) 332apply (simp add: monofun_cfun) 333apply (simp add: rev_below_trans [OF lower_plus_below1]) 334apply simp 335done 336 337definition 338 lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where 339 "lower_bind = lower_pd.extension lower_bind_basis" 340 341syntax 342 "_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic" 343 ("(3\<Union>\<flat>_\<in>_./ _)" [0, 0, 10] 10) 344 345translations 346 "\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)" 347 348lemma lower_bind_principal [simp]: 349 "lower_bind\<cdot>(lower_principal t) = lower_bind_basis t" 350unfolding lower_bind_def 351apply (rule lower_pd.extension_principal) 352apply (erule lower_bind_basis_mono) 353done 354 355lemma lower_bind_unit [simp]: 356 "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x" 357by (induct x rule: compact_basis.principal_induct, simp, simp) 358 359lemma lower_bind_plus [simp]: 360 "lower_bind\<cdot>(xs \<union>\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f \<union>\<flat> lower_bind\<cdot>ys\<cdot>f" 361by (induct xs rule: lower_pd.principal_induct, simp, 362 induct ys rule: lower_pd.principal_induct, simp, simp) 363 364lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" 365unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit) 366 367lemma lower_bind_bind: 368 "lower_bind\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_bind\<cdot>(f\<cdot>x)\<cdot>g)" 369by (induct xs, simp_all) 370 371 372subsection \<open>Map\<close> 373 374definition 375 lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where 376 "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))" 377 378lemma lower_map_unit [simp]: 379 "lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>" 380unfolding lower_map_def by simp 381 382lemma lower_map_plus [simp]: 383 "lower_map\<cdot>f\<cdot>(xs \<union>\<flat> ys) = lower_map\<cdot>f\<cdot>xs \<union>\<flat> lower_map\<cdot>f\<cdot>ys" 384unfolding lower_map_def by simp 385 386lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>" 387unfolding lower_map_def by simp 388 389lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs" 390by (induct xs rule: lower_pd_induct, simp_all) 391 392lemma lower_map_ID: "lower_map\<cdot>ID = ID" 393by (simp add: cfun_eq_iff ID_def lower_map_ident) 394 395lemma lower_map_map: 396 "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs" 397by (induct xs rule: lower_pd_induct, simp_all) 398 399lemma lower_bind_map: 400 "lower_bind\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))" 401by (simp add: lower_map_def lower_bind_bind) 402 403lemma lower_map_bind: 404 "lower_map\<cdot>f\<cdot>(lower_bind\<cdot>xs\<cdot>g) = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_map\<cdot>f\<cdot>(g\<cdot>x))" 405by (simp add: lower_map_def lower_bind_bind) 406 407lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)" 408apply standard 409apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse) 410apply (induct_tac y rule: lower_pd_induct) 411apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff) 412done 413 414lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)" 415apply standard 416apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem) 417apply (induct_tac x rule: lower_pd_induct) 418apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff) 419done 420 421(* FIXME: long proof! *) 422lemma finite_deflation_lower_map: 423 assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)" 424proof (rule finite_deflation_intro) 425 interpret d: finite_deflation d by fact 426 from d.deflation_axioms show "deflation (lower_map\<cdot>d)" 427 by (rule deflation_lower_map) 428 have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range) 429 hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))" 430 by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject) 431 hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp 432 hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" 433 by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject) 434 hence *: "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp 435 hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))" 436 apply (rule rev_finite_subset) 437 apply clarsimp 438 apply (induct_tac xs rule: lower_pd.principal_induct) 439 apply (simp add: adm_mem_finite *) 440 apply (rename_tac t, induct_tac t rule: pd_basis_induct) 441 apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit) 442 apply simp 443 apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b") 444 apply clarsimp 445 apply (rule imageI) 446 apply (rule vimageI2) 447 apply (simp add: Rep_PDUnit) 448 apply (rule range_eqI) 449 apply (erule sym) 450 apply (rule exI) 451 apply (rule Abs_compact_basis_inverse [symmetric]) 452 apply (simp add: d.compact) 453 apply (simp only: lower_plus_principal [symmetric] lower_map_plus) 454 apply clarsimp 455 apply (rule imageI) 456 apply (rule vimageI2) 457 apply (simp add: Rep_PDPlus) 458 done 459 thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}" 460 by (rule finite_range_imp_finite_fixes) 461qed 462 463subsection \<open>Lower powerdomain is bifinite\<close> 464 465lemma approx_chain_lower_map: 466 assumes "approx_chain a" 467 shows "approx_chain (\<lambda>i. lower_map\<cdot>(a i))" 468 using assms unfolding approx_chain_def 469 by (simp add: lub_APP lower_map_ID finite_deflation_lower_map) 470 471instance lower_pd :: (bifinite) bifinite 472proof 473 show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a" 474 using bifinite [where 'a='a] 475 by (fast intro!: approx_chain_lower_map) 476qed 477 478subsection \<open>Join\<close> 479 480definition 481 lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where 482 "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" 483 484lemma lower_join_unit [simp]: 485 "lower_join\<cdot>{xs}\<flat> = xs" 486unfolding lower_join_def by simp 487 488lemma lower_join_plus [simp]: 489 "lower_join\<cdot>(xss \<union>\<flat> yss) = lower_join\<cdot>xss \<union>\<flat> lower_join\<cdot>yss" 490unfolding lower_join_def by simp 491 492lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>" 493unfolding lower_join_def by simp 494 495lemma lower_join_map_unit: 496 "lower_join\<cdot>(lower_map\<cdot>lower_unit\<cdot>xs) = xs" 497by (induct xs rule: lower_pd_induct, simp_all) 498 499lemma lower_join_map_join: 500 "lower_join\<cdot>(lower_map\<cdot>lower_join\<cdot>xsss) = lower_join\<cdot>(lower_join\<cdot>xsss)" 501by (induct xsss rule: lower_pd_induct, simp_all) 502 503lemma lower_join_map_map: 504 "lower_join\<cdot>(lower_map\<cdot>(lower_map\<cdot>f)\<cdot>xss) = 505 lower_map\<cdot>f\<cdot>(lower_join\<cdot>xss)" 506by (induct xss rule: lower_pd_induct, simp_all) 507 508end 509