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 696locale boolean_algebra_cancel 697begin 698 699lemma sup1: "(A::'a::semilattice_sup) \<equiv> sup k a \<Longrightarrow> sup A b \<equiv> sup k (sup a b)" 700 by (simp only: ac_simps) 701 702lemma sup2: "(B::'a::semilattice_sup) \<equiv> sup k b \<Longrightarrow> sup a B \<equiv> sup k (sup a b)" 703 by (simp only: ac_simps) 704 705lemma sup0: "(a::'a::bounded_semilattice_sup_bot) \<equiv> sup a bot" 706 by simp 707 708lemma inf1: "(A::'a::semilattice_inf) \<equiv> inf k a \<Longrightarrow> inf A b \<equiv> inf k (inf a b)" 709 by (simp only: ac_simps) 710 711lemma inf2: "(B::'a::semilattice_inf) \<equiv> inf k b \<Longrightarrow> inf a B \<equiv> inf k (inf a b)" 712 by (simp only: ac_simps) 713 714lemma inf0: "(a::'a::bounded_semilattice_inf_top) \<equiv> inf a top" 715 by simp 716 717end 718 719ML_file \<open>Tools/boolean_algebra_cancel.ML\<close> 720 721simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") = 722 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close> 723 724simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = 725 \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close> 726 727 728subsection \<open>\<open>min/max\<close> as special case of lattice\<close> 729 730context linorder 731begin 732 733sublocale min: semilattice_order min less_eq less 734 + max: semilattice_order max greater_eq greater 735 by standard (auto simp add: min_def max_def) 736 737lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" 738 unfolding min_def using linear by (auto intro: order_trans) 739 740lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" 741 unfolding max_def using linear by (auto intro: order_trans) 742 743lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z" 744 unfolding min_def le_less using less_linear by (auto intro: less_trans) 745 746lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y" 747 unfolding max_def le_less using less_linear by (auto intro: less_trans) 748 749lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y" 750 unfolding min_def le_less using less_linear by (auto intro: less_trans) 751 752lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z" 753 unfolding max_def le_less using less_linear by (auto intro: less_trans) 754 755lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" 756 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 757 758lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" 759 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 760 761lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" 762 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 763 764lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" 765 by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) 766 767lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 768 769lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" 770 by (simp add: min_def) 771 772lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" 773 by (simp add: max_def) 774 775lemma split_min_lin [no_atp]: 776 \<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close> 777 by (cases a b rule: linorder_cases) (auto simp add: min.absorb1 min.absorb2) 778 779lemma split_max_lin [no_atp]: 780 \<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close> 781 by (cases a b rule: linorder_cases) (auto simp add: max.absorb1 max.absorb2) 782 783lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder" 784 by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) 785 786lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder" 787 by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) 788 789end 790 791lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)" 792 and min_of_antimono: "antimono f \<Longrightarrow> min (f x) (f y) = f (max x y)" 793 for f::"'a::linorder \<Rightarrow> 'b::linorder" 794 by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym) 795 796lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 797 by (auto intro: antisym simp add: min_def fun_eq_iff) 798 799lemma sup_max: "sup = (max :: 'a::{semilattice_sup,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 800 by (auto intro: antisym simp add: max_def fun_eq_iff) 801 802 803subsection \<open>Uniqueness of inf and sup\<close> 804 805lemma (in semilattice_inf) inf_unique: 806 fixes f (infixl "\<triangle>" 70) 807 assumes le1: "\<And>x y. x \<triangle> y \<le> x" 808 and le2: "\<And>x y. x \<triangle> y \<le> y" 809 and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 810 shows "x \<sqinter> y = x \<triangle> y" 811proof (rule antisym) 812 show "x \<triangle> y \<le> x \<sqinter> y" 813 by (rule le_infI) (rule le1, rule le2) 814 have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" 815 by (blast intro: greatest) 816 show "x \<sqinter> y \<le> x \<triangle> y" 817 by (rule leI) simp_all 818qed 819 820lemma (in semilattice_sup) sup_unique: 821 fixes f (infixl "\<nabla>" 70) 822 assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" 823 and ge2: "\<And>x y. y \<le> x \<nabla> y" 824 and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x" 825 shows "x \<squnion> y = x \<nabla> y" 826proof (rule antisym) 827 show "x \<squnion> y \<le> x \<nabla> y" 828 by (rule le_supI) (rule ge1, rule ge2) 829 have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" 830 by (blast intro: least) 831 show "x \<nabla> y \<le> x \<squnion> y" 832 by (rule leI) simp_all 833qed 834 835 836subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close> 837 838instantiation bool :: boolean_algebra 839begin 840 841definition bool_Compl_def [simp]: "uminus = Not" 842 843definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B" 844 845definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 846 847definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" 848 849instance by standard auto 850 851end 852 853lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q" 854 by simp 855 856lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q" 857 by simp 858 859lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 860 by auto 861 862 863subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close> 864 865instantiation "fun" :: (type, semilattice_sup) semilattice_sup 866begin 867 868definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 869 870lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x" 871 by (simp add: sup_fun_def) 872 873instance 874 by standard (simp_all add: le_fun_def) 875 876end 877 878instantiation "fun" :: (type, semilattice_inf) semilattice_inf 879begin 880 881definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 882 883lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x" 884 by (simp add: inf_fun_def) 885 886instance by standard (simp_all add: le_fun_def) 887 888end 889 890instance "fun" :: (type, lattice) lattice .. 891 892instance "fun" :: (type, distrib_lattice) distrib_lattice 893 by standard (rule ext, simp add: sup_inf_distrib1) 894 895instance "fun" :: (type, bounded_lattice) bounded_lattice .. 896 897instantiation "fun" :: (type, uminus) uminus 898begin 899 900definition fun_Compl_def: "- A = (\<lambda>x. - A x)" 901 902lemma uminus_apply [simp, code]: "(- A) x = - (A x)" 903 by (simp add: fun_Compl_def) 904 905instance .. 906 907end 908 909instantiation "fun" :: (type, minus) minus 910begin 911 912definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)" 913 914lemma minus_apply [simp, code]: "(A - B) x = A x - B x" 915 by (simp add: fun_diff_def) 916 917instance .. 918 919end 920 921instance "fun" :: (type, boolean_algebra) boolean_algebra 922 by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ 923 924 925subsection \<open>Lattice on unary and binary predicates\<close> 926 927lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" 928 by (simp add: inf_fun_def) 929 930lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y" 931 by (simp add: inf_fun_def) 932 933lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P" 934 by (simp add: inf_fun_def) 935 936lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P" 937 by (simp add: inf_fun_def) 938 939lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" 940 by (rule inf1E) 941 942lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" 943 by (rule inf2E) 944 945lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" 946 by (rule inf1E) 947 948lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" 949 by (rule inf2E) 950 951lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x" 952 by (simp add: sup_fun_def) 953 954lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y" 955 by (simp add: sup_fun_def) 956 957lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x" 958 by (simp add: sup_fun_def) 959 960lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y" 961 by (simp add: sup_fun_def) 962 963lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P" 964 by (simp add: sup_fun_def) iprover 965 966lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P" 967 by (simp add: sup_fun_def) iprover 968 969text \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close> 970 971lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x" 972 by (auto simp add: sup_fun_def) 973 974lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" 975 by (auto simp add: sup_fun_def) 976 977end 978