1(* Title: HOL/Lattice/CompleteLattice.thy 2 Author: Markus Wenzel, TU Muenchen 3*) 4 5section \<open>Complete lattices\<close> 6 7theory CompleteLattice imports Lattice begin 8 9subsection \<open>Complete lattice operations\<close> 10 11text \<open> 12 A \emph{complete lattice} is a partial order with general 13 (infinitary) infimum of any set of elements. General supremum 14 exists as well, as a consequence of the connection of infinitary 15 bounds (see \S\ref{sec:connect-bounds}). 16\<close> 17 18class complete_lattice = 19 assumes ex_Inf: "\<exists>inf. is_Inf A inf" 20 21theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup" 22proof - 23 from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast 24 then have "is_Sup A sup" by (rule Inf_Sup) 25 then show ?thesis .. 26qed 27 28text \<open> 29 The general \<open>\<Sqinter>\<close> (meet) and \<open>\<Squnion>\<close> (join) operations select 30 such infimum and supremum elements. 31\<close> 32 33definition 34 Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) where 35 "\<Sqinter>A = (THE inf. is_Inf A inf)" 36definition 37 Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) where 38 "\<Squnion>A = (THE sup. is_Sup A sup)" 39 40text \<open> 41 Due to unique existence of bounds, the complete lattice operations 42 may be exhibited as follows. 43\<close> 44 45lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf" 46proof (unfold Meet_def) 47 assume "is_Inf A inf" 48 then show "(THE inf. is_Inf A inf) = inf" 49 by (rule the_equality) (rule is_Inf_uniq [OF _ \<open>is_Inf A inf\<close>]) 50qed 51 52lemma MeetI [intro?]: 53 "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow> 54 (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow> 55 \<Sqinter>A = inf" 56 by (rule Meet_equality, rule is_InfI) blast+ 57 58lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup" 59proof (unfold Join_def) 60 assume "is_Sup A sup" 61 then show "(THE sup. is_Sup A sup) = sup" 62 by (rule the_equality) (rule is_Sup_uniq [OF _ \<open>is_Sup A sup\<close>]) 63qed 64 65lemma JoinI [intro?]: 66 "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow> 67 (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow> 68 \<Squnion>A = sup" 69 by (rule Join_equality, rule is_SupI) blast+ 70 71 72text \<open> 73 \medskip The \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations indeed determine 74 bounds on a complete lattice structure. 75\<close> 76 77lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)" 78proof (unfold Meet_def) 79 from ex_Inf obtain inf where "is_Inf A inf" .. 80 then show "is_Inf A (THE inf. is_Inf A inf)" 81 by (rule theI) (rule is_Inf_uniq [OF _ \<open>is_Inf A inf\<close>]) 82qed 83 84lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A" 85 by (rule is_Inf_greatest, rule is_Inf_Meet) blast 86 87lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a" 88 by (rule is_Inf_lower) (rule is_Inf_Meet) 89 90 91lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)" 92proof (unfold Join_def) 93 from ex_Sup obtain sup where "is_Sup A sup" .. 94 then show "is_Sup A (THE sup. is_Sup A sup)" 95 by (rule theI) (rule is_Sup_uniq [OF _ \<open>is_Sup A sup\<close>]) 96qed 97 98lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x" 99 by (rule is_Sup_least, rule is_Sup_Join) blast 100lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A" 101 by (rule is_Sup_upper) (rule is_Sup_Join) 102 103 104subsection \<open>The Knaster-Tarski Theorem\<close> 105 106text \<open> 107 The Knaster-Tarski Theorem (in its simplest formulation) states that 108 any monotone function on a complete lattice has a least fixed-point 109 (see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example). This 110 is a consequence of the basic boundary properties of the complete 111 lattice operations. 112\<close> 113 114theorem Knaster_Tarski: 115 assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" 116 obtains a :: "'a::complete_lattice" where 117 "f a = a" and "\<And>a'. f a' = a' \<Longrightarrow> a \<sqsubseteq> a'" 118proof 119 let ?H = "{u. f u \<sqsubseteq> u}" 120 let ?a = "\<Sqinter>?H" 121 show "f ?a = ?a" 122 proof - 123 have ge: "f ?a \<sqsubseteq> ?a" 124 proof 125 fix x assume x: "x \<in> ?H" 126 then have "?a \<sqsubseteq> x" .. 127 then have "f ?a \<sqsubseteq> f x" by (rule mono) 128 also from x have "... \<sqsubseteq> x" .. 129 finally show "f ?a \<sqsubseteq> x" . 130 qed 131 also have "?a \<sqsubseteq> f ?a" 132 proof 133 from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono) 134 then show "f ?a \<in> ?H" .. 135 qed 136 finally show ?thesis . 137 qed 138 139 fix a' 140 assume "f a' = a'" 141 then have "f a' \<sqsubseteq> a'" by (simp only: leq_refl) 142 then have "a' \<in> ?H" .. 143 then show "?a \<sqsubseteq> a'" .. 144qed 145 146theorem Knaster_Tarski_dual: 147 assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" 148 obtains a :: "'a::complete_lattice" where 149 "f a = a" and "\<And>a'. f a' = a' \<Longrightarrow> a' \<sqsubseteq> a" 150proof 151 let ?H = "{u. u \<sqsubseteq> f u}" 152 let ?a = "\<Squnion>?H" 153 show "f ?a = ?a" 154 proof - 155 have le: "?a \<sqsubseteq> f ?a" 156 proof 157 fix x assume x: "x \<in> ?H" 158 then have "x \<sqsubseteq> f x" .. 159 also from x have "x \<sqsubseteq> ?a" .. 160 then have "f x \<sqsubseteq> f ?a" by (rule mono) 161 finally show "x \<sqsubseteq> f ?a" . 162 qed 163 have "f ?a \<sqsubseteq> ?a" 164 proof 165 from le have "f ?a \<sqsubseteq> f (f ?a)" by (rule mono) 166 then show "f ?a \<in> ?H" .. 167 qed 168 from this and le show ?thesis by (rule leq_antisym) 169 qed 170 171 fix a' 172 assume "f a' = a'" 173 then have "a' \<sqsubseteq> f a'" by (simp only: leq_refl) 174 then have "a' \<in> ?H" .. 175 then show "a' \<sqsubseteq> ?a" .. 176qed 177 178 179subsection \<open>Bottom and top elements\<close> 180 181text \<open> 182 With general bounds available, complete lattices also have least and 183 greatest elements. 184\<close> 185 186definition 187 bottom :: "'a::complete_lattice" ("\<bottom>") where 188 "\<bottom> = \<Sqinter>UNIV" 189 190definition 191 top :: "'a::complete_lattice" ("\<top>") where 192 "\<top> = \<Squnion>UNIV" 193 194lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x" 195proof (unfold bottom_def) 196 have "x \<in> UNIV" .. 197 then show "\<Sqinter>UNIV \<sqsubseteq> x" .. 198qed 199 200lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x" 201proof (unfold bottom_def) 202 assume "\<And>a. x \<sqsubseteq> a" 203 show "\<Sqinter>UNIV = x" 204 proof 205 fix a show "x \<sqsubseteq> a" by fact 206 next 207 fix b :: "'a::complete_lattice" 208 assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a" 209 have "x \<in> UNIV" .. 210 with b show "b \<sqsubseteq> x" .. 211 qed 212qed 213 214lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>" 215proof (unfold top_def) 216 have "x \<in> UNIV" .. 217 then show "x \<sqsubseteq> \<Squnion>UNIV" .. 218qed 219 220lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x" 221proof (unfold top_def) 222 assume "\<And>a. a \<sqsubseteq> x" 223 show "\<Squnion>UNIV = x" 224 proof 225 fix a show "a \<sqsubseteq> x" by fact 226 next 227 fix b :: "'a::complete_lattice" 228 assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b" 229 have "x \<in> UNIV" .. 230 with b show "x \<sqsubseteq> b" .. 231 qed 232qed 233 234 235subsection \<open>Duality\<close> 236 237text \<open> 238 The class of complete lattices is closed under formation of dual 239 structures. 240\<close> 241 242instance dual :: (complete_lattice) complete_lattice 243proof 244 fix A' :: "'a::complete_lattice dual set" 245 show "\<exists>inf'. is_Inf A' inf'" 246 proof - 247 have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup) 248 then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf) 249 then show ?thesis by (simp add: dual_ex [symmetric] image_comp) 250 qed 251qed 252 253text \<open> 254 Apparently, the \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations are dual to each 255 other. 256\<close> 257 258theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)" 259proof - 260 from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" .. 261 then have "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" .. 262 then show ?thesis .. 263qed 264 265theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)" 266proof - 267 from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" .. 268 then have "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" .. 269 then show ?thesis .. 270qed 271 272text \<open> 273 Likewise are \<open>\<bottom>\<close> and \<open>\<top>\<close> duals of each other. 274\<close> 275 276theorem dual_bottom [intro?]: "dual \<bottom> = \<top>" 277proof - 278 have "\<top> = dual \<bottom>" 279 proof 280 fix a' have "\<bottom> \<sqsubseteq> undual a'" .. 281 then have "dual (undual a') \<sqsubseteq> dual \<bottom>" .. 282 then show "a' \<sqsubseteq> dual \<bottom>" by simp 283 qed 284 then show ?thesis .. 285qed 286 287theorem dual_top [intro?]: "dual \<top> = \<bottom>" 288proof - 289 have "\<bottom> = dual \<top>" 290 proof 291 fix a' have "undual a' \<sqsubseteq> \<top>" .. 292 then have "dual \<top> \<sqsubseteq> dual (undual a')" .. 293 then show "dual \<top> \<sqsubseteq> a'" by simp 294 qed 295 then show ?thesis .. 296qed 297 298 299subsection \<open>Complete lattices are lattices\<close> 300 301text \<open> 302 Complete lattices (with general bounds available) are indeed plain 303 lattices as well. This holds due to the connection of general 304 versus binary bounds that has been formally established in 305 \S\ref{sec:gen-bin-bounds}. 306\<close> 307 308lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})" 309proof - 310 have "is_Inf {x, y} (\<Sqinter>{x, y})" .. 311 then show ?thesis by (simp only: is_Inf_binary) 312qed 313 314lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})" 315proof - 316 have "is_Sup {x, y} (\<Squnion>{x, y})" .. 317 then show ?thesis by (simp only: is_Sup_binary) 318qed 319 320instance complete_lattice \<subseteq> lattice 321proof 322 fix x y :: "'a::complete_lattice" 323 from is_inf_binary show "\<exists>inf. is_inf x y inf" .. 324 from is_sup_binary show "\<exists>sup. is_sup x y sup" .. 325qed 326 327theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}" 328 by (rule meet_equality) (rule is_inf_binary) 329 330theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}" 331 by (rule join_equality) (rule is_sup_binary) 332 333 334subsection \<open>Complete lattices and set-theory operations\<close> 335 336text \<open> 337 The complete lattice operations are (anti) monotone wrt.\ set 338 inclusion. 339\<close> 340 341theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" 342proof (rule Meet_greatest) 343 fix a assume "a \<in> A" 344 also assume "A \<subseteq> B" 345 finally have "a \<in> B" . 346 then show "\<Sqinter>B \<sqsubseteq> a" .. 347qed 348 349theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B" 350proof - 351 assume "A \<subseteq> B" 352 then have "dual ` A \<subseteq> dual ` B" by blast 353 then have "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono) 354 then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join) 355 then show ?thesis by (simp only: dual_leq) 356qed 357 358text \<open> 359 Bounds over unions of sets may be obtained separately. 360\<close> 361 362theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" 363proof 364 fix a assume "a \<in> A \<union> B" 365 then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a" 366 proof 367 assume a: "a \<in> A" 368 have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" .. 369 also from a have "\<dots> \<sqsubseteq> a" .. 370 finally show ?thesis . 371 next 372 assume a: "a \<in> B" 373 have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" .. 374 also from a have "\<dots> \<sqsubseteq> a" .. 375 finally show ?thesis . 376 qed 377next 378 fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a" 379 show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B" 380 proof 381 show "b \<sqsubseteq> \<Sqinter>A" 382 proof 383 fix a assume "a \<in> A" 384 then have "a \<in> A \<union> B" .. 385 with b show "b \<sqsubseteq> a" .. 386 qed 387 show "b \<sqsubseteq> \<Sqinter>B" 388 proof 389 fix a assume "a \<in> B" 390 then have "a \<in> A \<union> B" .. 391 with b show "b \<sqsubseteq> a" .. 392 qed 393 qed 394qed 395 396theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" 397proof - 398 have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual ` A \<union> dual ` B)" 399 by (simp only: dual_Join image_Un) 400 also have "\<dots> = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)" 401 by (rule Meet_Un) 402 also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)" 403 by (simp only: dual_join dual_Join) 404 finally show ?thesis .. 405qed 406 407text \<open> 408 Bounds over singleton sets are trivial. 409\<close> 410 411theorem Meet_singleton: "\<Sqinter>{x} = x" 412proof 413 fix a assume "a \<in> {x}" 414 then have "a = x" by simp 415 then show "x \<sqsubseteq> a" by (simp only: leq_refl) 416next 417 fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a" 418 then show "b \<sqsubseteq> x" by simp 419qed 420 421theorem Join_singleton: "\<Squnion>{x} = x" 422proof - 423 have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join) 424 also have "\<dots> = dual x" by (rule Meet_singleton) 425 finally show ?thesis .. 426qed 427 428text \<open> 429 Bounds over the empty and universal set correspond to each other. 430\<close> 431 432theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV" 433proof 434 fix a :: "'a::complete_lattice" 435 assume "a \<in> {}" 436 then have False by simp 437 then show "\<Squnion>UNIV \<sqsubseteq> a" .. 438next 439 fix b :: "'a::complete_lattice" 440 have "b \<in> UNIV" .. 441 then show "b \<sqsubseteq> \<Squnion>UNIV" .. 442qed 443 444theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV" 445proof - 446 have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join) 447 also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty) 448 also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet) 449 finally show ?thesis .. 450qed 451 452end 453