1(* Title: HOL/Lattices.thy 2 Author: Tobias Nipkow 3*) 4 5section \<open>Abstract lattices\<close> 6 7theory Lattices 8imports Groups 9begin 10 11subsection \<open>Abstract semilattice\<close> 12 13text \<open> 14 These locales provide a basic structure for interpretation into 15 bigger structures; extensions require careful thinking, otherwise 16 undesired effects may occur due to interpretation. 17\<close> 18 19locale semilattice = abel_semigroup + 20 assumes idem [simp]: "a \<^bold>* a = a" 21begin 22 23lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b" 24 by (simp add: assoc [symmetric]) 25 26lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b" 27 by (simp add: assoc) 28 29end 30 31locale semilattice_neutr = semilattice + comm_monoid 32 33locale semilattice_order = semilattice + 34 fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50) 35 and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50) 36 assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b" 37 and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b" 38begin 39 40lemma orderI: "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b" 41 by (simp add: order_iff) 42 43lemma orderE: 44 assumes "a \<^bold>\<le> b" 45 obtains "a = a \<^bold>* b" 46 using assms by (unfold order_iff) 47 48sublocale ordering less_eq less 49proof 50 show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b 51 by (simp add: order_iff strict_order_iff) 52next 53 show "a \<^bold>\<le> a" for a 54 by (simp add: order_iff) 55next 56 fix a b 57 assume "a \<^bold>\<le> b" "b \<^bold>\<le> a" 58 then have "a = a \<^bold>* b" "a \<^bold>* b = b" 59 by (simp_all add: order_iff commute) 60 then show "a = b" by simp 61next 62 fix a b c 63 assume "a \<^bold>\<le> b" "b \<^bold>\<le> c" 64 then have "a = a \<^bold>* b" "b = b \<^bold>* c" 65 by (simp_all add: order_iff commute) 66 then have "a = a \<^bold>* (b \<^bold>* c)" 67 by simp 68 then have "a = (a \<^bold>* b) \<^bold>* c" 69 by (simp add: assoc) 70 with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp 71 then show "a \<^bold>\<le> c" by (rule orderI) 72qed 73 74lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\<le> a" 75 by (simp add: order_iff commute) 76 77lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\<le> b" 78 by (simp add: order_iff) 79 80lemma boundedI: 81 assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c" 82 shows "a \<^bold>\<le> b \<^bold>* c" 83proof (rule orderI) 84 from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a" 85 by (auto elim!: orderE) 86 then show "a = a \<^bold>* (b \<^bold>* c)" 87 by (simp add: assoc [symmetric]) 88qed 89 90lemma boundedE: 91 assumes "a \<^bold>\<le> b \<^bold>* c" 92 obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c" 93 using assms by (blast intro: trans cobounded1 cobounded2) 94 95lemma bounded_iff [simp]: "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c" 96 by (blast intro: boundedI elim: boundedE) 97 98lemma strict_boundedE: 99 assumes "a \<^bold>< b \<^bold>* c" 100 obtains "a \<^bold>< b" and "a \<^bold>< c" 101 using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+ 102 103lemma coboundedI1: "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c" 104 by (rule trans) auto 105 106lemma coboundedI2: "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c" 107 by (rule trans) auto 108 109lemma strict_coboundedI1: "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c" 110 using irrefl 111 by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order 112 elim: strict_boundedE) 113 114lemma strict_coboundedI2: "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c" 115 using strict_coboundedI1 [of b c a] by (simp add: commute) 116 117lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d" 118 by (blast intro: boundedI coboundedI1 coboundedI2) 119 120lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a" 121 by (rule antisym) (auto simp: refl) 122 123lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b" 124 by (rule antisym) (auto simp: refl) 125 126lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a" 127 using order_iff by auto 128 129lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b" 130 using order_iff by (auto simp add: commute) 131 132end 133 134locale semilattice_neutr_order = semilattice_neutr + semilattice_order 135begin 136 137sublocale ordering_top less_eq less "\<^bold>1" 138 by standard (simp add: order_iff) 139 140end 141 142text \<open>Passive interpretations for boolean operators\<close> 143 144lemma semilattice_neutr_and: 145 "semilattice_neutr HOL.conj True" 146 by standard auto 147 148lemma semilattice_neutr_or: 149 "semilattice_neutr HOL.disj False" 150 by standard auto 151 152 153subsection \<open>Syntactic infimum and supremum operations\<close> 154 155class inf = 156 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) 157 158class sup = 159 fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) 160 161 162subsection \<open>Concrete lattices\<close> 163 164class semilattice_inf = order + inf + 165 assumes inf_le1 [simp]: "x \<sqinter> y \<le> x" 166 and inf_le2 [simp]: "x \<sqinter> y \<le> y" 167 and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z" 168 169class semilattice_sup = order + sup + 170 assumes sup_ge1 [simp]: "x \<le> x \<squnion> y" 171 and sup_ge2 [simp]: "y \<le> x \<squnion> y" 172 and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x" 173begin 174 175text \<open>Dual lattice.\<close> 176lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater" 177 by (rule class.semilattice_inf.intro, rule dual_order) 178 (unfold_locales, simp_all add: sup_least) 179 180end 181 182class lattice = semilattice_inf + semilattice_sup 183 184 185subsubsection \<open>Intro and elim rules\<close> 186 187context semilattice_inf 188begin 189 190lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x" 191 by (rule order_trans) auto 192 193lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x" 194 by (rule order_trans) auto 195 196lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b" 197 by (fact inf_greatest) (* FIXME: duplicate lemma *) 198 199lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P" 200 by (blast intro: order_trans inf_le1 inf_le2) 201 202lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z" 203 by (blast intro: le_infI elim: le_infE) 204 205lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x" 206 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff) 207 208lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d" 209 by (fast intro: inf_greatest le_infI1 le_infI2) 210 211lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf" 212 by (auto simp add: mono_def intro: Lattices.inf_greatest) 213 214end 215 216context semilattice_sup 217begin 218 219lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b" 220 by (rule order_trans) auto 221 222lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b" 223 by (rule order_trans) auto 224 225lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x" 226 by (fact sup_least) (* FIXME: duplicate lemma *) 227 228lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 229 by (blast intro: order_trans sup_ge1 sup_ge2) 230 231lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z" 232 by (blast intro: le_supI elim: le_supE) 233 234lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y" 235 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff) 236 237lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d" 238 by (fast intro: sup_least le_supI1 le_supI2) 239 240lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup" 241 by (auto simp add: mono_def intro: Lattices.sup_least) 242 243end 244 245 246subsubsection \<open>Equational laws\<close> 247 248context semilattice_inf 249begin 250 251sublocale inf: semilattice inf 252proof 253 fix a b c 254 show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" 255 by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff) 256 show "a \<sqinter> b = b \<sqinter> a" 257 by (rule antisym) (auto simp add: le_inf_iff) 258 show "a \<sqinter> a = a" 259 by (rule antisym) (auto simp add: le_inf_iff) 260qed 261 262sublocale inf: semilattice_order inf less_eq less 263 by standard (auto simp add: le_iff_inf less_le) 264 265lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 266 by (fact inf.assoc) 267 268lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" 269 by (fact inf.commute) 270 271lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" 272 by (fact inf.left_commute) 273 274lemma inf_idem: "x \<sqinter> x = x" 275 by (fact inf.idem) (* already simp *) 276 277lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" 278 by (fact inf.left_idem) (* already simp *) 279 280lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y" 281 by (fact inf.right_idem) (* already simp *) 282 283lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x" 284 by (rule antisym) auto 285 286lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y" 287 by (rule antisym) auto 288 289lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem 290 291end 292 293context semilattice_sup 294begin 295 296sublocale sup: semilattice sup 297proof 298 fix a b c 299 show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" 300 by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) 301 show "a \<squnion> b = b \<squnion> a" 302 by (rule antisym) (auto simp add: le_sup_iff) 303 show "a \<squnion> a = a" 304 by (rule antisym) (auto simp add: le_sup_iff) 305qed 306 307sublocale sup: semilattice_order sup greater_eq greater 308 by standard (auto simp add: le_iff_sup sup.commute less_le) 309 310lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 311 by (fact sup.assoc) 312 313lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" 314 by (fact sup.commute) 315 316lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" 317 by (fact sup.left_commute) 318 319lemma sup_idem: "x \<squnion> x = x" 320 by (fact sup.idem) (* already simp *) 321 322lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" 323 by (fact sup.left_idem) 324 325lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x" 326 by (rule antisym) auto 327 328lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y" 329 by (rule antisym) auto 330 331lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem 332 333end 334 335context lattice 336begin 337 338lemma dual_lattice: "class.lattice sup (\<ge>) (>) inf" 339 by (rule class.lattice.intro, 340 rule dual_semilattice, 341 rule class.semilattice_sup.intro, 342 rule dual_order) 343 (unfold_locales, auto) 344 345lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x" 346 by (blast intro: antisym inf_le1 inf_greatest sup_ge1) 347 348lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x" 349 by (blast intro: antisym sup_ge1 sup_least inf_le1) 350 351lemmas inf_sup_aci = inf_aci sup_aci 352 353lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 354 355text \<open>Towards distributivity.\<close> 356 357lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)" 358 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 359 360lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)" 361 by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 362 363text \<open>If you have one of them, you have them all.\<close> 364 365lemma distrib_imp1: 366 assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 367 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 368proof- 369 have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" 370 by simp 371 also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" 372 by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb) 373 also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" 374 by (simp add: inf_commute) 375 also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib) 376 finally show ?thesis . 377qed 378 379lemma distrib_imp2: 380 assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 381 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 382proof- 383 have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" 384 by simp 385 also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" 386 by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb) 387 also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" 388 by (simp add: sup_commute) 389 also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib) 390 finally show ?thesis . 391qed 392 393end 394 395 396subsubsection \<open>Strict order\<close> 397 398context semilattice_inf 399begin 400 401lemma less_infI1: "a < x \<Longrightarrow> a \<sqinter> b < x" 402 by (auto simp add: less_le inf_absorb1 intro: le_infI1) 403 404lemma less_infI2: "b < x \<Longrightarrow> a \<sqinter> b < x" 405 by (auto simp add: less_le inf_absorb2 intro: le_infI2) 406 407end 408 409context semilattice_sup 410begin 411 412lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b" 413 using dual_semilattice 414 by (rule semilattice_inf.less_infI1) 415 416lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b" 417 using dual_semilattice 418 by (rule semilattice_inf.less_infI2) 419 420end 421 422 423subsection \<open>Distributive lattices\<close> 424 425class distrib_lattice = lattice + 426 assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 427 428context distrib_lattice 429begin 430 431lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" 432 by (simp add: sup_commute sup_inf_distrib1) 433 434lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 435 by (rule distrib_imp2 [OF sup_inf_distrib1]) 436 437lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 438 by (simp add: inf_commute inf_sup_distrib1) 439 440lemma dual_distrib_lattice: "class.distrib_lattice sup (\<ge>) (>) inf" 441 by (rule class.distrib_lattice.intro, rule dual_lattice) 442 (unfold_locales, fact inf_sup_distrib1) 443 444lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2 445 446lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2 447 448lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 449 450end 451 452 453subsection \<open>Bounded lattices and boolean algebras\<close> 454 455class bounded_semilattice_inf_top = semilattice_inf + order_top 456begin 457 458sublocale inf_top: semilattice_neutr inf top 459 + inf_top: semilattice_neutr_order inf top less_eq less 460proof 461 show "x \<sqinter> \<top> = x" for x 462 by (rule inf_absorb1) simp 463qed 464 465end 466 467class bounded_semilattice_sup_bot = semilattice_sup + order_bot 468begin 469 470sublocale sup_bot: semilattice_neutr sup bot 471 + sup_bot: semilattice_neutr_order sup bot greater_eq greater 472proof 473 show "x \<squnion> \<bottom> = x" for x 474 by (rule sup_absorb1) simp 475qed 476 477end 478 479class bounded_lattice_bot = lattice + order_bot 480begin 481 482subclass bounded_semilattice_sup_bot .. 483 484lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>" 485 by (rule inf_absorb1) simp 486 487lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>" 488 by (rule inf_absorb2) simp 489 490lemma sup_bot_left: "\<bottom> \<squnion> x = x" 491 by (fact sup_bot.left_neutral) 492 493lemma sup_bot_right: "x \<squnion> \<bottom> = x" 494 by (fact sup_bot.right_neutral) 495 496lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" 497 by (simp add: eq_iff) 498 499lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" 500 by (simp add: eq_iff) 501 502end 503 504class bounded_lattice_top = lattice + order_top 505begin 506 507subclass bounded_semilattice_inf_top .. 508 509lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>" 510 by (rule sup_absorb1) simp 511 512lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>" 513 by (rule sup_absorb2) simp 514 515lemma inf_top_left: "\<top> \<sqinter> x = x" 516 by (fact inf_top.left_neutral) 517 518lemma inf_top_right: "x \<sqinter> \<top> = x" 519 by (fact inf_top.right_neutral) 520 521lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" 522 by (simp add: eq_iff) 523 524end 525 526class bounded_lattice = lattice + order_bot + order_top 527begin 528 529subclass bounded_lattice_bot .. 530subclass bounded_lattice_top .. 531 532lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>" 533 by unfold_locales (auto simp add: less_le_not_le) 534 535end 536 537class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + 538 assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>" 539 and sup_compl_top: "x \<squnion> - x = \<top>" 540 assumes diff_eq: "x - y = x \<sqinter> - y" 541begin 542 543lemma dual_boolean_algebra: 544 "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>" 545 by (rule class.boolean_algebra.intro, 546 rule dual_bounded_lattice, 547 rule dual_distrib_lattice) 548 (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) 549 550lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>" 551 by (simp add: inf_commute inf_compl_bot) 552 553lemma compl_sup_top [simp]: "- x \<squnion> x = \<top>" 554 by (simp add: sup_commute sup_compl_top) 555 556lemma compl_unique: 557 assumes "x \<sqinter> y = \<bottom>" 558 and "x \<squnion> y = \<top>" 559 shows "- x = y" 560proof - 561 have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)" 562 using inf_compl_bot assms(1) by simp 563 then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)" 564 by (simp add: inf_commute) 565 then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)" 566 by (simp add: inf_sup_distrib1) 567 then have "- x \<sqinter> \<top> = y \<sqinter> \<top>" 568 using sup_compl_top assms(2) by simp 569 then show "- x = y" by simp 570qed 571 572lemma double_compl [simp]: "- (- x) = x" 573 using compl_inf_bot compl_sup_top by (rule compl_unique) 574 575lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y" 576proof 577 assume "- x = - y" 578 then have "- (- x) = - (- y)" by (rule arg_cong) 579 then show "x = y" by simp 580next 581 assume "x = y" 582 then show "- x = - y" by simp 583qed 584 585lemma compl_bot_eq [simp]: "- \<bottom> = \<top>" 586proof - 587 from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" . 588 then show ?thesis by simp 589qed 590 591lemma compl_top_eq [simp]: "- \<top> = \<bottom>" 592proof - 593 from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" . 594 then show ?thesis by simp 595qed 596 597lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y" 598proof (rule compl_unique) 599 have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" 600 by (simp only: inf_sup_distrib inf_aci) 601 then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>" 602 by (simp add: inf_compl_bot) 603next 604 have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))" 605 by (simp only: sup_inf_distrib sup_aci) 606 then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>" 607 by (simp add: sup_compl_top) 608qed 609 610lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y" 611 using dual_boolean_algebra 612 by (rule boolean_algebra.compl_inf) 613 614lemma compl_mono: 615 assumes "x \<le> y" 616 shows "- y \<le> - x" 617proof - 618 from assms have "x \<squnion> y = y" by (simp only: le_iff_sup) 619 then have "- (x \<squnion> y) = - y" by simp 620 then have "- x \<sqinter> - y = - y" by simp 621 then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) 622 then show ?thesis by (simp only: le_iff_inf) 623qed 624 625lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x" 626 by (auto dest: compl_mono) 627 628lemma compl_le_swap1: 629 assumes "y \<le> - x" 630 shows "x \<le> -y" 631proof - 632 from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff) 633 then show ?thesis by simp 634qed 635 636lemma compl_le_swap2: 637 assumes "- y \<le> x" 638 shows "- x \<le> y" 639proof - 640 from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff) 641 then show ?thesis by simp 642qed 643 644lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x" (* TODO: declare [simp] ? *) 645 by (auto simp add: less_le) 646 647lemma compl_less_swap1: 648 assumes "y < - x" 649 shows "x < - y" 650proof - 651 from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff) 652 then show ?thesis by simp 653qed 654 655lemma compl_less_swap2: 656 assumes "- y < x" 657 shows "- x < y" 658proof - 659 from assms have "- x < - (- y)" 660 by (simp only: compl_less_compl_iff) 661 then show ?thesis by simp 662qed 663 664lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top" 665 by (simp add: inf_sup_aci sup_compl_top) 666 667lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top" 668 by (simp add: inf_sup_aci sup_compl_top) 669 670lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot" 671 by (simp add: inf_sup_aci inf_compl_bot) 672 673lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot" 674 by (simp add: inf_sup_aci inf_compl_bot) 675 676declare inf_compl_bot [simp] 677 and sup_compl_top [simp] 678 679lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top" 680 by (simp add: sup_assoc[symmetric]) 681 682lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top" 683 using sup_compl_top_left1[of "- x" y] by simp 684 685lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot" 686 by (simp add: inf_assoc[symmetric]) 687 688lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot" 689 using inf_compl_bot_left1[of "- x" y] by simp 690 691lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot" 692 by (subst inf_left_commute) simp 693 694end 695 696ML_file "Tools/boolean_algebra_cancel.ML" 697 698simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = 699 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close> 700 701simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = 702 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close> 703 704 705subsection \<open>\<open>min/max\<close> as special case of lattice\<close> 706 707context linorder 708begin 709 710sublocale min: semilattice_order min less_eq less 711 + max: semilattice_order max greater_eq greater 712 by standard (auto simp add: min_def max_def) 713 714lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" 715 unfolding min_def using linear by (auto intro: order_trans) 716 717lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" 718 unfolding max_def using linear by (auto intro: order_trans) 719 720lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z" 721 unfolding min_def le_less using less_linear by (auto intro: less_trans) 722 723lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y" 724 unfolding max_def le_less using less_linear by (auto intro: less_trans) 725 726lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y" 727 unfolding min_def le_less using less_linear by (auto intro: less_trans) 728 729lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z" 730 unfolding max_def le_less using less_linear by (auto intro: less_trans) 731 732lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" 733 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 734 735lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" 736 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 737 738lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" 739 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 740 741lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" 742 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 743 744lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 745 746lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" 747 by (simp add: min_def) 748 749lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" 750 by (simp add: max_def) 751 752lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder" 753 by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) 754 755lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder" 756 by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) 757 758end 759 760lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)" 761 and min_of_antimono: "antimono f \<Longrightarrow> min (f x) (f y) = f (max x y)" 762 for f::"'a::linorder \<Rightarrow> 'b::linorder" 763 by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym) 764 765lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 766 by (auto intro: antisym simp add: min_def fun_eq_iff) 767 768lemma sup_max: "sup = (max :: 'a::{semilattice_sup,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 769 by (auto intro: antisym simp add: max_def fun_eq_iff) 770 771 772subsection \<open>Uniqueness of inf and sup\<close> 773 774lemma (in semilattice_inf) inf_unique: 775 fixes f (infixl "\<triangle>" 70) 776 assumes le1: "\<And>x y. x \<triangle> y \<le> x" 777 and le2: "\<And>x y. x \<triangle> y \<le> y" 778 and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 779 shows "x \<sqinter> y = x \<triangle> y" 780proof (rule antisym) 781 show "x \<triangle> y \<le> x \<sqinter> y" 782 by (rule le_infI) (rule le1, rule le2) 783 have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 784 by (blast intro: greatest) 785 show "x \<sqinter> y \<le> x \<triangle> y" 786 by (rule leI) simp_all 787qed 788 789lemma (in semilattice_sup) sup_unique: 790 fixes f (infixl "\<nabla>" 70) 791 assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" 792 and ge2: "\<And>x y. y \<le> x \<nabla> y" 793 and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" 794 shows "x \<squnion> y = x \<nabla> y" 795proof (rule antisym) 796 show "x \<squnion> y \<le> x \<nabla> y" 797 by (rule le_supI) (rule ge1, rule ge2) 798 have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" 799 by (blast intro: least) 800 show "x \<nabla> y \<le> x \<squnion> y" 801 by (rule leI) simp_all 802qed 803 804 805subsection \<open>Lattice on @{typ bool}\<close> 806 807instantiation bool :: boolean_algebra 808begin 809 810definition bool_Compl_def [simp]: "uminus = Not" 811 812definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B" 813 814definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 815 816definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" 817 818instance by standard auto 819 820end 821 822lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q" 823 by simp 824 825lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q" 826 by simp 827 828lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 829 by auto 830 831 832subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close> 833 834instantiation "fun" :: (type, semilattice_sup) semilattice_sup 835begin 836 837definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 838 839lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x" 840 by (simp add: sup_fun_def) 841 842instance 843 by standard (simp_all add: le_fun_def) 844 845end 846 847instantiation "fun" :: (type, semilattice_inf) semilattice_inf 848begin 849 850definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 851 852lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x" 853 by (simp add: inf_fun_def) 854 855instance by standard (simp_all add: le_fun_def) 856 857end 858 859instance "fun" :: (type, lattice) lattice .. 860 861instance "fun" :: (type, distrib_lattice) distrib_lattice 862 by standard (rule ext, simp add: sup_inf_distrib1) 863 864instance "fun" :: (type, bounded_lattice) bounded_lattice .. 865 866instantiation "fun" :: (type, uminus) uminus 867begin 868 869definition fun_Compl_def: "- A = (\<lambda>x. - A x)" 870 871lemma uminus_apply [simp, code]: "(- A) x = - (A x)" 872 by (simp add: fun_Compl_def) 873 874instance .. 875 876end 877 878instantiation "fun" :: (type, minus) minus 879begin 880 881definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)" 882 883lemma minus_apply [simp, code]: "(A - B) x = A x - B x" 884 by (simp add: fun_diff_def) 885 886instance .. 887 888end 889 890instance "fun" :: (type, boolean_algebra) boolean_algebra 891 by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ 892 893 894subsection \<open>Lattice on unary and binary predicates\<close> 895 896lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" 897 by (simp add: inf_fun_def) 898 899lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y" 900 by (simp add: inf_fun_def) 901 902lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P" 903 by (simp add: inf_fun_def) 904 905lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P" 906 by (simp add: inf_fun_def) 907 908lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" 909 by (rule inf1E) 910 911lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" 912 by (rule inf2E) 913 914lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" 915 by (rule inf1E) 916 917lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" 918 by (rule inf2E) 919 920lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x" 921 by (simp add: sup_fun_def) 922 923lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y" 924 by (simp add: sup_fun_def) 925 926lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x" 927 by (simp add: sup_fun_def) 928 929lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y" 930 by (simp add: sup_fun_def) 931 932lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P" 933 by (simp add: sup_fun_def) iprover 934 935lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P" 936 by (simp add: sup_fun_def) iprover 937 938text \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close> 939 940lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x" 941 by (auto simp add: sup_fun_def) 942 943lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" 944 by (auto simp add: sup_fun_def) 945 946end 947