1(* Title: HOL/HOLCF/Deflation.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Continuous deflations and ep-pairs\<close> 6 7theory Deflation 8 imports Cfun 9begin 10 11default_sort cpo 12 13 14subsection \<open>Continuous deflations\<close> 15 16locale deflation = 17 fixes d :: "'a \<rightarrow> 'a" 18 assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x" 19 assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x" 20begin 21 22lemma below_ID: "d \<sqsubseteq> ID" 23 by (rule cfun_belowI) (simp add: below) 24 25text \<open>The set of fixed points is the same as the range.\<close> 26 27lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)" 28 by (auto simp add: eq_sym_conv idem) 29 30lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}" 31 by (auto simp add: eq_sym_conv idem) 32 33text \<open> 34 The pointwise ordering on deflation functions coincides with 35 the subset ordering of their sets of fixed-points. 36\<close> 37 38lemma belowI: 39 assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" 40 shows "d \<sqsubseteq> f" 41proof (rule cfun_belowI) 42 fix x 43 from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" 44 by (rule monofun_cfun_arg) 45 also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" 46 by (rule f) 47 finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" . 48qed 49 50lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x" 51proof (rule below_antisym) 52 from below show "d\<cdot>x \<sqsubseteq> x" . 53 assume "f \<sqsubseteq> d" 54 then have "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun) 55 also assume "f\<cdot>x = x" 56 finally show "x \<sqsubseteq> d\<cdot>x" . 57qed 58 59end 60 61lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>" 62 by (rule deflation.below [THEN bottomI]) 63 64lemma adm_deflation: "adm (\<lambda>d. deflation d)" 65 by (simp add: deflation_def) 66 67lemma deflation_ID: "deflation ID" 68 by (simp add: deflation.intro) 69 70lemma deflation_bottom: "deflation \<bottom>" 71 by (simp add: deflation.intro) 72 73lemma deflation_below_iff: "deflation p \<Longrightarrow> deflation q \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)" 74 apply safe 75 apply (simp add: deflation.belowD) 76 apply (simp add: deflation.belowI) 77 done 78 79text \<open> 80 The composition of two deflations is equal to 81 the lesser of the two (if they are comparable). 82\<close> 83 84lemma deflation_below_comp1: 85 assumes "deflation f" 86 assumes "deflation g" 87 shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x" 88proof (rule below_antisym) 89 interpret g: deflation g by fact 90 from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg) 91next 92 interpret f: deflation f by fact 93 assume "f \<sqsubseteq> g" 94 then have "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun) 95 then have "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg) 96 also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem) 97 finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" . 98qed 99 100lemma deflation_below_comp2: "deflation f \<Longrightarrow> deflation g \<Longrightarrow> f \<sqsubseteq> g \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x" 101 by (simp only: deflation.belowD deflation.idem) 102 103 104subsection \<open>Deflations with finite range\<close> 105 106lemma finite_range_imp_finite_fixes: 107 assumes "finite (range f)" 108 shows "finite {x. f x = x}" 109proof - 110 have "{x. f x = x} \<subseteq> range f" 111 by (clarify, erule subst, rule rangeI) 112 from this assms show "finite {x. f x = x}" 113 by (rule finite_subset) 114qed 115 116locale finite_deflation = deflation + 117 assumes finite_fixes: "finite {x. d\<cdot>x = x}" 118begin 119 120lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))" 121 by (simp add: range_eq_fixes finite_fixes) 122 123lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)" 124 by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range]) 125 126lemma compact: "compact (d\<cdot>x)" 127proof (rule compactI2) 128 fix Y :: "nat \<Rightarrow> 'a" 129 assume Y: "chain Y" 130 have "finite_chain (\<lambda>i. d\<cdot>(Y i))" 131 proof (rule finite_range_imp_finch) 132 from Y show "chain (\<lambda>i. d\<cdot>(Y i))" by simp 133 have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)" by auto 134 then show "finite (range (\<lambda>i. d\<cdot>(Y i)))" 135 using finite_range by (rule finite_subset) 136 qed 137 then have "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" 138 by (simp add: finite_chain_def maxinch_is_thelub Y) 139 then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" .. 140 141 assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)" 142 then have "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)" 143 by (rule monofun_cfun_arg) 144 then have "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))" 145 by (simp add: contlub_cfun_arg Y idem) 146 with j have "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)" by simp 147 then have "d\<cdot>x \<sqsubseteq> Y j" 148 using below by (rule below_trans) 149 then show "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" .. 150qed 151 152end 153 154lemma finite_deflation_intro: "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d" 155 by (intro finite_deflation.intro finite_deflation_axioms.intro) 156 157lemma finite_deflation_imp_deflation: "finite_deflation d \<Longrightarrow> deflation d" 158 by (simp add: finite_deflation_def) 159 160lemma finite_deflation_bottom: "finite_deflation \<bottom>" 161 by standard simp_all 162 163 164subsection \<open>Continuous embedding-projection pairs\<close> 165 166locale ep_pair = 167 fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a" 168 assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x" 169 and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y" 170begin 171 172lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y" 173proof 174 assume "e\<cdot>x \<sqsubseteq> e\<cdot>y" 175 then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg) 176 then show "x \<sqsubseteq> y" by simp 177next 178 assume "x \<sqsubseteq> y" 179 then show "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg) 180qed 181 182lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y" 183 unfolding po_eq_conv e_below_iff .. 184 185lemma p_eq_iff: "e\<cdot>(p\<cdot>x) = x \<Longrightarrow> e\<cdot>(p\<cdot>y) = y \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y" 186 by (safe, erule subst, erule subst, simp) 187 188lemma p_inverse: "(\<exists>x. y = e\<cdot>x) \<longleftrightarrow> e\<cdot>(p\<cdot>y) = y" 189 by (auto, rule exI, erule sym) 190 191lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y" 192proof 193 assume "e\<cdot>x \<sqsubseteq> y" 194 then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg) 195 then show "x \<sqsubseteq> p\<cdot>y" by simp 196next 197 assume "x \<sqsubseteq> p\<cdot>y" 198 then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg) 199 then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans) 200qed 201 202lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x" 203proof - 204 assume "compact (e\<cdot>x)" 205 then have "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD) 206 then have "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2]) 207 then have "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp 208 then show "compact x" by (rule compactI) 209qed 210 211lemma compact_e: 212 assumes "compact x" 213 shows "compact (e\<cdot>x)" 214proof - 215 from assms have "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD) 216 then have "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2]) 217 then have "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p) 218 then show "compact (e\<cdot>x)" by (rule compactI) 219qed 220 221lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x" 222 by (rule iffI [OF compact_e_rev compact_e]) 223 224text \<open>Deflations from ep-pairs\<close> 225 226lemma deflation_e_p: "deflation (e oo p)" 227 by (simp add: deflation.intro e_p_below) 228 229lemma deflation_e_d_p: 230 assumes "deflation d" 231 shows "deflation (e oo d oo p)" 232proof 233 interpret deflation d by fact 234 fix x :: 'b 235 show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x" 236 by (simp add: idem) 237 show "(e oo d oo p)\<cdot>x \<sqsubseteq> x" 238 by (simp add: e_below_iff_below_p below) 239qed 240 241lemma finite_deflation_e_d_p: 242 assumes "finite_deflation d" 243 shows "finite_deflation (e oo d oo p)" 244proof 245 interpret finite_deflation d by fact 246 fix x :: 'b 247 show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x" 248 by (simp add: idem) 249 show "(e oo d oo p)\<cdot>x \<sqsubseteq> x" 250 by (simp add: e_below_iff_below_p below) 251 have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))" 252 by (simp add: finite_image) 253 then have "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))" 254 by (simp add: image_image) 255 then show "finite {x. (e oo d oo p)\<cdot>x = x}" 256 by (rule finite_range_imp_finite_fixes) 257qed 258 259lemma deflation_p_d_e: 260 assumes "deflation d" 261 assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)" 262 shows "deflation (p oo d oo e)" 263proof - 264 interpret d: deflation d by fact 265 have p_d_e_below: "(p oo d oo e)\<cdot>x \<sqsubseteq> x" for x 266 proof - 267 have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x" 268 by (rule d.below) 269 then have "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)" 270 by (rule monofun_cfun_arg) 271 then show ?thesis by simp 272 qed 273 show ?thesis 274 proof 275 show "(p oo d oo e)\<cdot>x \<sqsubseteq> x" for x 276 by (rule p_d_e_below) 277 show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x" for x 278 proof (rule below_antisym) 279 show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x" 280 by (rule p_d_e_below) 281 have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))" 282 by (intro monofun_cfun_arg d) 283 then have "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))" 284 by (simp only: d.idem) 285 then show "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)" 286 by simp 287 qed 288 qed 289qed 290 291lemma finite_deflation_p_d_e: 292 assumes "finite_deflation d" 293 assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)" 294 shows "finite_deflation (p oo d oo e)" 295proof - 296 interpret d: finite_deflation d by fact 297 show ?thesis 298 proof (rule finite_deflation_intro) 299 have "deflation d" .. 300 then show "deflation (p oo d oo e)" 301 using d by (rule deflation_p_d_e) 302 next 303 have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))" 304 by (rule d.finite_image) 305 then have "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))" 306 by (rule finite_imageI) 307 then have "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))" 308 by (simp add: image_image) 309 then show "finite {x. (p oo d oo e)\<cdot>x = x}" 310 by (rule finite_range_imp_finite_fixes) 311 qed 312qed 313 314end 315 316subsection \<open>Uniqueness of ep-pairs\<close> 317 318lemma ep_pair_unique_e_lemma: 319 assumes 1: "ep_pair e1 p" 320 and 2: "ep_pair e2 p" 321 shows "e1 \<sqsubseteq> e2" 322proof (rule cfun_belowI) 323 fix x 324 have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x" 325 by (rule ep_pair.e_p_below [OF 1]) 326 then show "e1\<cdot>x \<sqsubseteq> e2\<cdot>x" 327 by (simp only: ep_pair.e_inverse [OF 2]) 328qed 329 330lemma ep_pair_unique_e: "ep_pair e1 p \<Longrightarrow> ep_pair e2 p \<Longrightarrow> e1 = e2" 331 by (fast intro: below_antisym elim: ep_pair_unique_e_lemma) 332 333lemma ep_pair_unique_p_lemma: 334 assumes 1: "ep_pair e p1" 335 and 2: "ep_pair e p2" 336 shows "p1 \<sqsubseteq> p2" 337proof (rule cfun_belowI) 338 fix x 339 have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x" 340 by (rule ep_pair.e_p_below [OF 1]) 341 then have "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x" 342 by (rule monofun_cfun_arg) 343 then show "p1\<cdot>x \<sqsubseteq> p2\<cdot>x" 344 by (simp only: ep_pair.e_inverse [OF 2]) 345qed 346 347lemma ep_pair_unique_p: "ep_pair e p1 \<Longrightarrow> ep_pair e p2 \<Longrightarrow> p1 = p2" 348 by (fast intro: below_antisym elim: ep_pair_unique_p_lemma) 349 350 351subsection \<open>Composing ep-pairs\<close> 352 353lemma ep_pair_ID_ID: "ep_pair ID ID" 354 by standard simp_all 355 356lemma ep_pair_comp: 357 assumes "ep_pair e1 p1" and "ep_pair e2 p2" 358 shows "ep_pair (e2 oo e1) (p1 oo p2)" 359proof 360 interpret ep1: ep_pair e1 p1 by fact 361 interpret ep2: ep_pair e2 p2 by fact 362 fix x y 363 show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x" 364 by simp 365 have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y" 366 by (rule ep1.e_p_below) 367 then have "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)" 368 by (rule monofun_cfun_arg) 369 also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y" 370 by (rule ep2.e_p_below) 371 finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y" 372 by simp 373qed 374 375locale pcpo_ep_pair = ep_pair e p 376 for e :: "'a::pcpo \<rightarrow> 'b::pcpo" 377 and p :: "'b::pcpo \<rightarrow> 'a::pcpo" 378begin 379 380lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>" 381proof - 382 have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal) 383 then have "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg) 384 also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below) 385 finally show "e\<cdot>\<bottom> = \<bottom>" by simp 386qed 387 388lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>" 389 by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict]) 390 391lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>" 392 by simp 393 394lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>" 395 by (rule e_inverse [where x="\<bottom>", unfolded e_strict]) 396 397lemmas stricts = e_strict p_strict 398 399end 400 401end 402