src/HOL/Algebra/Lattice.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 67443 3abf6a722518 child 69700 7a92cbec7030 permissions -rw-r--r--
More on Algebra by Paulo and Martin
 wenzelm@35849 1 (* Title: HOL/Algebra/Lattice.thy wenzelm@35849 2 Author: Clemens Ballarin, started 7 November 2003 wenzelm@35849 3 Copyright: Clemens Ballarin ballarin@27714 4 ballarin@27717 5 Most congruence rules by Stephan Hohe. ballarin@65099 6 With additional contributions from Alasdair Armstrong and Simon Foster. ballarin@14551 7 *) ballarin@14551 8 wenzelm@35849 9 theory Lattice ballarin@65099 10 imports Order wenzelm@44472 11 begin ballarin@27713 12 ballarin@65099 13 section \Lattices\ ballarin@65099 14 ballarin@65099 15 subsection \Supremum and infimum\ ballarin@27713 16 wenzelm@35847 17 definition ballarin@27713 18 sup :: "[_, 'a set] => 'a" ("\\_" [90] 90) wenzelm@35848 19 where "\\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))" ballarin@27713 20 wenzelm@35847 21 definition ballarin@27713 22 inf :: "[_, 'a set] => 'a" ("\\_" [90] 90) wenzelm@35848 23 where "\\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))" ballarin@27713 24 ballarin@65099 25 definition supr :: ballarin@65099 26 "('a, 'b) gorder_scheme \ 'c set \ ('c \ 'a) \ 'a " ballarin@65099 27 where "supr L A f = \\<^bsub>L\<^esub>(f  A)" ballarin@65099 28 ballarin@65099 29 definition infi :: ballarin@65099 30 "('a, 'b) gorder_scheme \ 'c set \ ('c \ 'a) \ 'a " ballarin@65099 31 where "infi L A f = \\<^bsub>L\<^esub>(f  A)" ballarin@65099 32 ballarin@65099 33 syntax ballarin@65099 34 "_inf1" :: "('a, 'b) gorder_scheme \ pttrns \ 'a \ 'a" ("(3IINF\ _./ _)" [0, 10] 10) ballarin@65099 35 "_inf" :: "('a, 'b) gorder_scheme \ pttrn \ 'c set \ 'a \ 'a" ("(3IINF\ _:_./ _)" [0, 0, 10] 10) ballarin@65099 36 "_sup1" :: "('a, 'b) gorder_scheme \ pttrns \ 'a \ 'a" ("(3SSUP\ _./ _)" [0, 10] 10) ballarin@65099 37 "_sup" :: "('a, 'b) gorder_scheme \ pttrn \ 'c set \ 'a \ 'a" ("(3SSUP\ _:_./ _)" [0, 0, 10] 10) ballarin@65099 38 ballarin@65099 39 translations ballarin@65099 40 "IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)" ballarin@65099 41 "IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)" ballarin@65099 42 "SSUP\<^bsub>L\<^esub> x. B" == "CONST supr L CONST UNIV (%x. B)" ballarin@65099 43 "SSUP\<^bsub>L\<^esub> x:A. B" == "CONST supr L A (%x. B)" ballarin@65099 44 wenzelm@35847 45 definition ballarin@27713 46 join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65) wenzelm@35848 47 where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}" ballarin@27713 48 wenzelm@35847 49 definition ballarin@27713 50 meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 70) wenzelm@35848 51 where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}" ballarin@27713 52 ballarin@65099 53 definition ballarin@66580 54 LEAST_FP :: "('a, 'b) gorder_scheme \ ('a \ 'a) \ 'a" ("LFP\") where wenzelm@67443 55 "LEAST_FP L f = \\<^bsub>L\<^esub> {u \ carrier L. f u \\<^bsub>L\<^esub> u}" \ \least fixed point\ ballarin@65099 56 ballarin@65099 57 definition ballarin@66580 58 GREATEST_FP:: "('a, 'b) gorder_scheme \ ('a \ 'a) \ 'a" ("GFP\") where wenzelm@67443 59 "GREATEST_FP L f = \\<^bsub>L\<^esub> {u \ carrier L. u \\<^bsub>L\<^esub> f u}" \ \greatest fixed point\ ballarin@65099 60 ballarin@65099 61 ballarin@65099 62 subsection \Dual operators\ ballarin@65099 63 ballarin@65099 64 lemma sup_dual [simp]: ballarin@65099 65 "\\<^bsub>inv_gorder L\<^esub>A = \\<^bsub>L\<^esub>A" ballarin@65099 66 by (simp add: sup_def inf_def) ballarin@65099 67 ballarin@65099 68 lemma inf_dual [simp]: ballarin@65099 69 "\\<^bsub>inv_gorder L\<^esub>A = \\<^bsub>L\<^esub>A" ballarin@65099 70 by (simp add: sup_def inf_def) ballarin@65099 71 ballarin@65099 72 lemma join_dual [simp]: ballarin@65099 73 "p \\<^bsub>inv_gorder L\<^esub> q = p \\<^bsub>L\<^esub> q" ballarin@65099 74 by (simp add:join_def meet_def) ballarin@65099 75 ballarin@65099 76 lemma meet_dual [simp]: ballarin@65099 77 "p \\<^bsub>inv_gorder L\<^esub> q = p \\<^bsub>L\<^esub> q" ballarin@65099 78 by (simp add:join_def meet_def) ballarin@65099 79 ballarin@65099 80 lemma top_dual [simp]: ballarin@65099 81 "\\<^bsub>inv_gorder L\<^esub> = \\<^bsub>L\<^esub>" ballarin@65099 82 by (simp add: top_def bottom_def) ballarin@65099 83 ballarin@65099 84 lemma bottom_dual [simp]: ballarin@65099 85 "\\<^bsub>inv_gorder L\<^esub> = \\<^bsub>L\<^esub>" ballarin@65099 86 by (simp add: top_def bottom_def) ballarin@65099 87 ballarin@65099 88 lemma LFP_dual [simp]: ballarin@66580 89 "LEAST_FP (inv_gorder L) f = GREATEST_FP L f" ballarin@66580 90 by (simp add:LEAST_FP_def GREATEST_FP_def) ballarin@65099 91 ballarin@65099 92 lemma GFP_dual [simp]: ballarin@66580 93 "GREATEST_FP (inv_gorder L) f = LEAST_FP L f" ballarin@66580 94 by (simp add:LEAST_FP_def GREATEST_FP_def) ballarin@65099 95 ballarin@27713 96 wenzelm@61382 97 subsection \Lattices\ ballarin@27713 98 ballarin@27713 99 locale weak_upper_semilattice = weak_partial_order + ballarin@27713 100 assumes sup_of_two_exists: wenzelm@67091 101 "[| x \ carrier L; y \ carrier L |] ==> \s. least L s (Upper L {x, y})" ballarin@27713 102 ballarin@27713 103 locale weak_lower_semilattice = weak_partial_order + ballarin@27713 104 assumes inf_of_two_exists: wenzelm@67091 105 "[| x \ carrier L; y \ carrier L |] ==> \s. greatest L s (Lower L {x, y})" ballarin@27713 106 ballarin@27713 107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice ballarin@27713 108 ballarin@65099 109 lemma (in weak_lattice) dual_weak_lattice: ballarin@65099 110 "weak_lattice (inv_gorder L)" ballarin@65099 111 proof - ballarin@65099 112 interpret dual: weak_partial_order "inv_gorder L" ballarin@65099 113 by (metis dual_weak_order) ballarin@65099 114 ballarin@65099 115 show ?thesis ballarin@65099 116 apply (unfold_locales) ballarin@65099 117 apply (simp_all add: inf_of_two_exists sup_of_two_exists) ballarin@65099 118 done ballarin@65099 119 qed ballarin@65099 120 wenzelm@14666 121 wenzelm@61382 122 subsubsection \Supremum\ ballarin@14551 123 ballarin@27713 124 lemma (in weak_upper_semilattice) joinI: ballarin@22063 125 "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ carrier L |] ballarin@14551 126 ==> P (x \ y)" ballarin@14551 127 proof (unfold join_def sup_def) ballarin@22063 128 assume L: "x \ carrier L" "y \ carrier L" ballarin@22063 129 and P: "!!l. least L l (Upper L {x, y}) ==> P l" ballarin@22063 130 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast ballarin@27713 131 with L show "P (SOME l. least L l (Upper L {x, y}))" ballarin@27713 132 by (fast intro: someI2 P) ballarin@14551 133 qed ballarin@14551 134 ballarin@27713 135 lemma (in weak_upper_semilattice) join_closed [simp]: ballarin@22063 136 "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L" ballarin@27700 137 by (rule joinI) (rule least_closed) ballarin@14551 138 ballarin@27713 139 lemma (in weak_upper_semilattice) join_cong_l: ballarin@27713 140 assumes carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L" ballarin@27713 141 and xx': "x .= x'" ballarin@27713 142 shows "x \ y .= x' \ y" ballarin@27713 143 proof (rule joinI, rule joinI) ballarin@27713 144 fix a b ballarin@27713 145 from xx' carr ballarin@27713 146 have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) ballarin@27713 147 ballarin@27713 148 assume leasta: "least L a (Upper L {x, y})" ballarin@27713 149 assume "least L b (Upper L {x', y})" ballarin@27713 150 with carr ballarin@27713 151 have leastb: "least L b (Upper L {x, y})" ballarin@27713 152 by (simp add: least_Upper_cong_r[OF _ _ seq]) ballarin@27713 153 ballarin@27713 154 from leasta leastb ballarin@27713 155 show "a .= b" by (rule weak_least_unique) ballarin@27713 156 qed (rule carr)+ ballarin@14551 157 ballarin@27713 158 lemma (in weak_upper_semilattice) join_cong_r: ballarin@27713 159 assumes carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L" ballarin@27713 160 and yy': "y .= y'" ballarin@27713 161 shows "x \ y .= x \ y'" ballarin@27713 162 proof (rule joinI, rule joinI) ballarin@27713 163 fix a b ballarin@27713 164 have "{x, y} = {y, x}" by fast ballarin@27713 165 also from carr yy' ballarin@27713 166 have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) ballarin@27713 167 also have "{y', x} = {x, y'}" by fast ballarin@27713 168 finally ballarin@27713 169 have seq: "{x, y} {.=} {x, y'}" . ballarin@14551 170 ballarin@27713 171 assume leasta: "least L a (Upper L {x, y})" ballarin@27713 172 assume "least L b (Upper L {x, y'})" ballarin@27713 173 with carr ballarin@27713 174 have leastb: "least L b (Upper L {x, y})" ballarin@27713 175 by (simp add: least_Upper_cong_r[OF _ _ seq]) ballarin@27713 176 ballarin@27713 177 from leasta leastb ballarin@27713 178 show "a .= b" by (rule weak_least_unique) ballarin@27713 179 qed (rule carr)+ ballarin@27713 180 ballarin@27713 181 lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *) ballarin@27713 182 "x \ carrier L ==> least L x (Upper L {x})" ballarin@27713 183 by (rule least_UpperI) auto ballarin@27713 184 ballarin@27713 185 lemma (in weak_partial_order) weak_sup_of_singleton [simp]: ballarin@27713 186 "x \ carrier L ==> \{x} .= x" ballarin@27713 187 unfolding sup_def ballarin@27713 188 by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI) ballarin@27713 189 ballarin@27713 190 lemma (in weak_partial_order) sup_of_singleton_closed [simp]: ballarin@27713 191 "x \ carrier L \ \{x} \ carrier L" ballarin@27713 192 unfolding sup_def ballarin@27713 193 by (rule someI2) (auto intro: sup_of_singletonI) wenzelm@14666 194 wenzelm@63167 195 text \Condition on \A\: supremum exists.\ ballarin@14551 196 ballarin@27713 197 lemma (in weak_upper_semilattice) sup_insertI: ballarin@22063 198 "[| !!s. least L s (Upper L (insert x A)) ==> P s; ballarin@22063 199 least L a (Upper L A); x \ carrier L; A \ carrier L |] wenzelm@14693 200 ==> P (\(insert x A))" ballarin@14551 201 proof (unfold sup_def) ballarin@22063 202 assume L: "x \ carrier L" "A \ carrier L" ballarin@22063 203 and P: "!!l. least L l (Upper L (insert x A)) ==> P l" ballarin@22063 204 and least_a: "least L a (Upper L A)" ballarin@22063 205 from L least_a have La: "a \ carrier L" by simp ballarin@14551 206 from L sup_of_two_exists least_a ballarin@22063 207 obtain s where least_s: "least L s (Upper L {a, x})" by blast ballarin@27713 208 show "P (SOME l. least L l (Upper L (insert x A)))" ballarin@27713 209 proof (rule someI2) ballarin@22063 210 show "least L s (Upper L (insert x A))" ballarin@14551 211 proof (rule least_UpperI) ballarin@14551 212 fix z wenzelm@14693 213 assume "z \ insert x A" wenzelm@14693 214 then show "z \ s" wenzelm@14693 215 proof wenzelm@14693 216 assume "z = x" then show ?thesis wenzelm@14693 217 by (simp add: least_Upper_above [OF least_s] L La) wenzelm@14693 218 next wenzelm@14693 219 assume "z \ A" wenzelm@14693 220 with L least_s least_a show ?thesis ballarin@27713 221 by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above) wenzelm@14693 222 qed wenzelm@14693 223 next wenzelm@14693 224 fix y ballarin@22063 225 assume y: "y \ Upper L (insert x A)" wenzelm@14693 226 show "s \ y" wenzelm@14693 227 proof (rule least_le [OF least_s], rule Upper_memI) wenzelm@32960 228 fix z wenzelm@32960 229 assume z: "z \ {a, x}" wenzelm@32960 230 then show "z \ y" wenzelm@32960 231 proof ballarin@22063 232 have y': "y \ Upper L A" ballarin@22063 233 apply (rule subsetD [where A = "Upper L (insert x A)"]) wenzelm@23463 234 apply (rule Upper_antimono) wenzelm@32960 235 apply blast wenzelm@32960 236 apply (rule y) wenzelm@14693 237 done wenzelm@14693 238 assume "z = a" wenzelm@14693 239 with y' least_a show ?thesis by (fast dest: least_le) wenzelm@32960 240 next wenzelm@32960 241 assume "z \ {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) wenzelm@14693 242 with y L show ?thesis by blast wenzelm@32960 243 qed wenzelm@23350 244 qed (rule Upper_closed [THEN subsetD, OF y]) wenzelm@14693 245 next ballarin@22063 246 from L show "insert x A \ carrier L" by simp ballarin@22063 247 from least_s show "s \ carrier L" by simp ballarin@14551 248 qed wenzelm@23350 249 qed (rule P) ballarin@14551 250 qed ballarin@14551 251 ballarin@27713 252 lemma (in weak_upper_semilattice) finite_sup_least: wenzelm@67091 253 "[| finite A; A \ carrier L; A \ {} |] ==> least L (\A) (Upper L A)" berghofe@22265 254 proof (induct set: finite) wenzelm@14693 255 case empty wenzelm@14693 256 then show ?case by simp ballarin@14551 257 next nipkow@15328 258 case (insert x A) ballarin@14551 259 show ?case ballarin@14551 260 proof (cases "A = {}") ballarin@14551 261 case True ballarin@27713 262 with insert show ?thesis wenzelm@44472 263 by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI) wenzelm@32960 264 (* The above step is hairy; least_cong can make simp loop. wenzelm@32960 265 Would want special version of simp to apply least_cong. *) ballarin@14551 266 next ballarin@14551 267 case False ballarin@22063 268 with insert have "least L (\A) (Upper L A)" by simp wenzelm@14693 269 with _ show ?thesis wenzelm@14693 270 by (rule sup_insertI) (simp_all add: insert [simplified]) ballarin@14551 271 qed ballarin@14551 272 qed ballarin@14551 273 ballarin@27713 274 lemma (in weak_upper_semilattice) finite_sup_insertI: ballarin@22063 275 assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" ballarin@22063 276 and xA: "finite A" "x \ carrier L" "A \ carrier L" ballarin@65099 277 shows "P (\ (insert x A))" ballarin@14551 278 proof (cases "A = {}") ballarin@14551 279 case True with P and xA show ?thesis ballarin@27713 280 by (simp add: finite_sup_least) ballarin@14551 281 next ballarin@14551 282 case False with P and xA show ?thesis ballarin@14551 283 by (simp add: sup_insertI finite_sup_least) ballarin@14551 284 qed ballarin@14551 285 ballarin@27713 286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]: wenzelm@67091 287 "[| finite A; A \ carrier L; A \ {} |] ==> \A \ carrier L" berghofe@22265 288 proof (induct set: finite) ballarin@14551 289 case empty then show ?case by simp ballarin@14551 290 next nipkow@15328 291 case insert then show ?case wenzelm@14693 292 by - (rule finite_sup_insertI, simp_all) ballarin@14551 293 qed ballarin@14551 294 ballarin@27713 295 lemma (in weak_upper_semilattice) join_left: ballarin@22063 296 "[| x \ carrier L; y \ carrier L |] ==> x \ x \ y" wenzelm@14693 297 by (rule joinI [folded join_def]) (blast dest: least_mem) ballarin@14551 298 ballarin@27713 299 lemma (in weak_upper_semilattice) join_right: ballarin@22063 300 "[| x \ carrier L; y \ carrier L |] ==> y \ x \ y" wenzelm@14693 301 by (rule joinI [folded join_def]) (blast dest: least_mem) ballarin@14551 302 ballarin@27713 303 lemma (in weak_upper_semilattice) sup_of_two_least: ballarin@22063 304 "[| x \ carrier L; y \ carrier L |] ==> least L (\{x, y}) (Upper L {x, y})" ballarin@14551 305 proof (unfold sup_def) ballarin@22063 306 assume L: "x \ carrier L" "y \ carrier L" ballarin@22063 307 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast ballarin@27713 308 with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})" ballarin@27713 309 by (fast intro: someI2 weak_least_unique) (* blast fails *) ballarin@14551 310 qed ballarin@14551 311 ballarin@27713 312 lemma (in weak_upper_semilattice) join_le: wenzelm@14693 313 assumes sub: "x \ z" "y \ z" wenzelm@23350 314 and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L" ballarin@14551 315 shows "x \ y \ z" wenzelm@23350 316 proof (rule joinI [OF _ x y]) ballarin@14551 317 fix s ballarin@22063 318 assume "least L s (Upper L {x, y})" wenzelm@23350 319 with sub z show "s \ z" by (fast elim: least_le intro: Upper_memI) ballarin@14551 320 qed wenzelm@14693 321 ballarin@65099 322 lemma (in weak_lattice) weak_le_iff_meet: ballarin@65099 323 assumes "x \ carrier L" "y \ carrier L" ballarin@65099 324 shows "x \ y \ (x \ y) .= y" ballarin@65099 325 by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym) ballarin@65099 326 ballarin@27713 327 lemma (in weak_upper_semilattice) weak_join_assoc_lemma: ballarin@22063 328 assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ballarin@27713 329 shows "x \ (y \ z) .= \{x, y, z}" ballarin@14551 330 proof (rule finite_sup_insertI) wenzelm@63167 331 \ \The textbook argument in Jacobson I, p 457\ ballarin@14551 332 fix s ballarin@22063 333 assume sup: "least L s (Upper L {x, y, z})" ballarin@27713 334 show "x \ (y \ z) .= s" nipkow@33657 335 proof (rule weak_le_antisym) ballarin@14551 336 from sup L show "x \ (y \ z) \ s" nipkow@44890 337 by (fastforce intro!: join_le elim: least_Upper_above) ballarin@14551 338 next ballarin@14551 339 from sup L show "s \ x \ (y \ z)" ballarin@14551 340 by (erule_tac least_le) ballarin@27713 341 (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed) ballarin@27700 342 qed (simp_all add: L least_closed [OF sup]) ballarin@14551 343 qed (simp_all add: L) ballarin@14551 344 wenzelm@63167 345 text \Commutativity holds for \=\.\ ballarin@27713 346 ballarin@22063 347 lemma join_comm: ballarin@22063 348 fixes L (structure) ballarin@22063 349 shows "x \ y = y \ x" ballarin@14551 350 by (unfold join_def) (simp add: insert_commute) ballarin@14551 351 ballarin@27713 352 lemma (in weak_upper_semilattice) weak_join_assoc: ballarin@22063 353 assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ballarin@27713 354 shows "(x \ y) \ z .= x \ (y \ z)" ballarin@14551 355 proof - ballarin@27713 356 (* FIXME: could be simplified by improved simp: uniform use of .=, ballarin@27713 357 omit [symmetric] in last step. *) ballarin@14551 358 have "(x \ y) \ z = z \ (x \ y)" by (simp only: join_comm) ballarin@27713 359 also from L have "... .= \{z, x, y}" by (simp add: weak_join_assoc_lemma) wenzelm@14693 360 also from L have "... = \{x, y, z}" by (simp add: insert_commute) ballarin@27713 361 also from L have "... .= x \ (y \ z)" by (simp add: weak_join_assoc_lemma [symmetric]) ballarin@27713 362 finally show ?thesis by (simp add: L) ballarin@14551 363 qed ballarin@14551 364 wenzelm@14693 365 wenzelm@61382 366 subsubsection \Infimum\ ballarin@14551 367 ballarin@27713 368 lemma (in weak_lower_semilattice) meetI: ballarin@22063 369 "[| !!i. greatest L i (Lower L {x, y}) ==> P i; ballarin@22063 370 x \ carrier L; y \ carrier L |] ballarin@14551 371 ==> P (x \ y)" ballarin@14551 372 proof (unfold meet_def inf_def) ballarin@22063 373 assume L: "x \ carrier L" "y \ carrier L" ballarin@22063 374 and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" ballarin@22063 375 with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast ballarin@27713 376 with L show "P (SOME g. greatest L g (Lower L {x, y}))" ballarin@27713 377 by (fast intro: someI2 weak_greatest_unique P) ballarin@14551 378 qed ballarin@14551 379 ballarin@27713 380 lemma (in weak_lower_semilattice) meet_closed [simp]: ballarin@22063 381 "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L" ballarin@27700 382 by (rule meetI) (rule greatest_closed) ballarin@14551 383 ballarin@27713 384 lemma (in weak_lower_semilattice) meet_cong_l: ballarin@27713 385 assumes carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L" ballarin@27713 386 and xx': "x .= x'" ballarin@27713 387 shows "x \ y .= x' \ y" ballarin@27713 388 proof (rule meetI, rule meetI) ballarin@27713 389 fix a b ballarin@27713 390 from xx' carr ballarin@27713 391 have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) ballarin@27713 392 ballarin@27713 393 assume greatesta: "greatest L a (Lower L {x, y})" ballarin@27713 394 assume "greatest L b (Lower L {x', y})" ballarin@27713 395 with carr ballarin@27713 396 have greatestb: "greatest L b (Lower L {x, y})" ballarin@27713 397 by (simp add: greatest_Lower_cong_r[OF _ _ seq]) ballarin@27713 398 ballarin@27713 399 from greatesta greatestb ballarin@27713 400 show "a .= b" by (rule weak_greatest_unique) ballarin@27713 401 qed (rule carr)+ ballarin@14551 402 ballarin@27713 403 lemma (in weak_lower_semilattice) meet_cong_r: ballarin@27713 404 assumes carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L" ballarin@27713 405 and yy': "y .= y'" ballarin@27713 406 shows "x \ y .= x \ y'" ballarin@27713 407 proof (rule meetI, rule meetI) ballarin@27713 408 fix a b ballarin@27713 409 have "{x, y} = {y, x}" by fast ballarin@27713 410 also from carr yy' ballarin@27713 411 have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) ballarin@27713 412 also have "{y', x} = {x, y'}" by fast ballarin@27713 413 finally ballarin@27713 414 have seq: "{x, y} {.=} {x, y'}" . ballarin@27713 415 ballarin@27713 416 assume greatesta: "greatest L a (Lower L {x, y})" ballarin@27713 417 assume "greatest L b (Lower L {x, y'})" ballarin@27713 418 with carr ballarin@27713 419 have greatestb: "greatest L b (Lower L {x, y})" ballarin@27713 420 by (simp add: greatest_Lower_cong_r[OF _ _ seq]) ballarin@14551 421 ballarin@27713 422 from greatesta greatestb ballarin@27713 423 show "a .= b" by (rule weak_greatest_unique) ballarin@27713 424 qed (rule carr)+ ballarin@27713 425 ballarin@27713 426 lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *) ballarin@27713 427 "x \ carrier L ==> greatest L x (Lower L {x})" ballarin@27713 428 by (rule greatest_LowerI) auto ballarin@14551 429 ballarin@27713 430 lemma (in weak_partial_order) weak_inf_of_singleton [simp]: ballarin@27713 431 "x \ carrier L ==> \{x} .= x" ballarin@27713 432 unfolding inf_def ballarin@27713 433 by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI) ballarin@27713 434 ballarin@27713 435 lemma (in weak_partial_order) inf_of_singleton_closed: ballarin@27713 436 "x \ carrier L ==> \{x} \ carrier L" ballarin@27713 437 unfolding inf_def ballarin@27713 438 by (rule someI2) (auto intro: inf_of_singletonI) ballarin@27713 439 wenzelm@63167 440 text \Condition on \A\: infimum exists.\ ballarin@27713 441 ballarin@27713 442 lemma (in weak_lower_semilattice) inf_insertI: ballarin@22063 443 "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; ballarin@22063 444 greatest L a (Lower L A); x \ carrier L; A \ carrier L |] wenzelm@14693 445 ==> P (\(insert x A))" ballarin@14551 446 proof (unfold inf_def) ballarin@22063 447 assume L: "x \ carrier L" "A \ carrier L" ballarin@22063 448 and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" ballarin@22063 449 and greatest_a: "greatest L a (Lower L A)" ballarin@22063 450 from L greatest_a have La: "a \ carrier L" by simp ballarin@14551 451 from L inf_of_two_exists greatest_a ballarin@22063 452 obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast ballarin@27713 453 show "P (SOME g. greatest L g (Lower L (insert x A)))" ballarin@27713 454 proof (rule someI2) ballarin@22063 455 show "greatest L i (Lower L (insert x A))" ballarin@14551 456 proof (rule greatest_LowerI) ballarin@14551 457 fix z wenzelm@14693 458 assume "z \ insert x A" wenzelm@14693 459 then show "i \ z" wenzelm@14693 460 proof wenzelm@14693 461 assume "z = x" then show ?thesis ballarin@27700 462 by (simp add: greatest_Lower_below [OF greatest_i] L La) wenzelm@14693 463 next wenzelm@14693 464 assume "z \ A" wenzelm@14693 465 with L greatest_i greatest_a show ?thesis ballarin@27713 466 by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below) wenzelm@14693 467 qed wenzelm@14693 468 next wenzelm@14693 469 fix y ballarin@22063 470 assume y: "y \ Lower L (insert x A)" wenzelm@14693 471 show "y \ i" wenzelm@14693 472 proof (rule greatest_le [OF greatest_i], rule Lower_memI) wenzelm@32960 473 fix z wenzelm@32960 474 assume z: "z \ {a, x}" wenzelm@32960 475 then show "y \ z" wenzelm@32960 476 proof ballarin@22063 477 have y': "y \ Lower L A" ballarin@22063 478 apply (rule subsetD [where A = "Lower L (insert x A)"]) wenzelm@23463 479 apply (rule Lower_antimono) wenzelm@32960 480 apply blast wenzelm@32960 481 apply (rule y) wenzelm@14693 482 done wenzelm@14693 483 assume "z = a" wenzelm@14693 484 with y' greatest_a show ?thesis by (fast dest: greatest_le) wenzelm@32960 485 next wenzelm@14693 486 assume "z \ {x}" wenzelm@14693 487 with y L show ?thesis by blast wenzelm@32960 488 qed wenzelm@23350 489 qed (rule Lower_closed [THEN subsetD, OF y]) wenzelm@14693 490 next ballarin@22063 491 from L show "insert x A \ carrier L" by simp ballarin@22063 492 from greatest_i show "i \ carrier L" by simp ballarin@14551 493 qed wenzelm@23350 494 qed (rule P) ballarin@14551 495 qed ballarin@14551 496 ballarin@27713 497 lemma (in weak_lower_semilattice) finite_inf_greatest: wenzelm@67091 498 "[| finite A; A \ carrier L; A \ {} |] ==> greatest L (\A) (Lower L A)" berghofe@22265 499 proof (induct set: finite) ballarin@14551 500 case empty then show ?case by simp ballarin@14551 501 next nipkow@15328 502 case (insert x A) ballarin@14551 503 show ?case ballarin@14551 504 proof (cases "A = {}") ballarin@14551 505 case True ballarin@27713 506 with insert show ?thesis ballarin@27713 507 by simp (simp add: greatest_cong [OF weak_inf_of_singleton] wenzelm@32960 508 inf_of_singleton_closed inf_of_singletonI) ballarin@14551 509 next ballarin@14551 510 case False ballarin@14551 511 from insert show ?thesis ballarin@14551 512 proof (rule_tac inf_insertI) ballarin@22063 513 from False insert show "greatest L (\A) (Lower L A)" by simp ballarin@14551 514 qed simp_all ballarin@14551 515 qed ballarin@14551 516 qed ballarin@14551 517 ballarin@27713 518 lemma (in weak_lower_semilattice) finite_inf_insertI: ballarin@22063 519 assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" ballarin@22063 520 and xA: "finite A" "x \ carrier L" "A \ carrier L" ballarin@65099 521 shows "P (\ (insert x A))" ballarin@14551 522 proof (cases "A = {}") ballarin@14551 523 case True with P and xA show ?thesis ballarin@27713 524 by (simp add: finite_inf_greatest) ballarin@14551 525 next ballarin@14551 526 case False with P and xA show ?thesis ballarin@14551 527 by (simp add: inf_insertI finite_inf_greatest) ballarin@14551 528 qed ballarin@14551 529 ballarin@27713 530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]: wenzelm@67091 531 "[| finite A; A \ carrier L; A \ {} |] ==> \A \ carrier L" berghofe@22265 532 proof (induct set: finite) ballarin@14551 533 case empty then show ?case by simp ballarin@14551 534 next nipkow@15328 535 case insert then show ?case ballarin@14551 536 by (rule_tac finite_inf_insertI) (simp_all) ballarin@14551 537 qed ballarin@14551 538 ballarin@27713 539 lemma (in weak_lower_semilattice) meet_left: ballarin@22063 540 "[| x \ carrier L; y \ carrier L |] ==> x \ y \ x" wenzelm@14693 541 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) ballarin@14551 542 ballarin@27713 543 lemma (in weak_lower_semilattice) meet_right: ballarin@22063 544 "[| x \ carrier L; y \ carrier L |] ==> x \ y \ y" wenzelm@14693 545 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) ballarin@14551 546 ballarin@27713 547 lemma (in weak_lower_semilattice) inf_of_two_greatest: ballarin@22063 548 "[| x \ carrier L; y \ carrier L |] ==> wenzelm@60585 549 greatest L (\{x, y}) (Lower L {x, y})" ballarin@14551 550 proof (unfold inf_def) ballarin@22063 551 assume L: "x \ carrier L" "y \ carrier L" ballarin@22063 552 with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast ballarin@14551 553 with L ballarin@27713 554 show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})" ballarin@27713 555 by (fast intro: someI2 weak_greatest_unique) (* blast fails *) ballarin@14551 556 qed ballarin@14551 557 ballarin@27713 558 lemma (in weak_lower_semilattice) meet_le: wenzelm@14693 559 assumes sub: "z \ x" "z \ y" wenzelm@23350 560 and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L" ballarin@14551 561 shows "z \ x \ y" wenzelm@23350 562 proof (rule meetI [OF _ x y]) ballarin@14551 563 fix i ballarin@22063 564 assume "greatest L i (Lower L {x, y})" wenzelm@23350 565 with sub z show "z \ i" by (fast elim: greatest_le intro: Lower_memI) ballarin@14551 566 qed wenzelm@14693 567 ballarin@65099 568 lemma (in weak_lattice) weak_le_iff_join: ballarin@65099 569 assumes "x \ carrier L" "y \ carrier L" ballarin@65099 570 shows "x \ y \ x .= (x \ y)" ballarin@65099 571 by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl) ballarin@65099 572 ballarin@27713 573 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma: ballarin@22063 574 assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ballarin@27713 575 shows "x \ (y \ z) .= \{x, y, z}" ballarin@14551 576 proof (rule finite_inf_insertI) wenzelm@61382 577 txt \The textbook argument in Jacobson I, p 457\ ballarin@14551 578 fix i ballarin@22063 579 assume inf: "greatest L i (Lower L {x, y, z})" ballarin@27713 580 show "x \ (y \ z) .= i" nipkow@33657 581 proof (rule weak_le_antisym) ballarin@14551 582 from inf L show "i \ x \ (y \ z)" nipkow@44890 583 by (fastforce intro!: meet_le elim: greatest_Lower_below) ballarin@14551 584 next ballarin@14551 585 from inf L show "x \ (y \ z) \ i" ballarin@14551 586 by (erule_tac greatest_le) ballarin@27713 587 (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed) ballarin@27700 588 qed (simp_all add: L greatest_closed [OF inf]) ballarin@14551 589 qed (simp_all add: L) ballarin@14551 590 ballarin@22063 591 lemma meet_comm: ballarin@22063 592 fixes L (structure) ballarin@22063 593 shows "x \ y = y \ x" ballarin@14551 594 by (unfold meet_def) (simp add: insert_commute) ballarin@14551 595 ballarin@27713 596 lemma (in weak_lower_semilattice) weak_meet_assoc: ballarin@22063 597 assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" ballarin@27713 598 shows "(x \ y) \ z .= x \ (y \ z)" ballarin@14551 599 proof - ballarin@27713 600 (* FIXME: improved simp, see weak_join_assoc above *) ballarin@14551 601 have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm) ballarin@65099 602 also from L have "... .= \ {z, x, y}" by (simp add: weak_meet_assoc_lemma) ballarin@65099 603 also from L have "... = \ {x, y, z}" by (simp add: insert_commute) ballarin@27713 604 also from L have "... .= x \ (y \ z)" by (simp add: weak_meet_assoc_lemma [symmetric]) ballarin@27713 605 finally show ?thesis by (simp add: L) ballarin@14551 606 qed ballarin@14551 607 wenzelm@61382 608 text \Total orders are lattices.\ ballarin@24087 609 ballarin@65099 610 sublocale weak_total_order \ weak?: weak_lattice haftmann@28823 611 proof ballarin@24087 612 fix x y ballarin@24087 613 assume L: "x \ carrier L" "y \ carrier L" wenzelm@67091 614 show "\s. least L s (Upper L {x, y})" ballarin@24087 615 proof - ballarin@24087 616 note total L ballarin@24087 617 moreover ballarin@24087 618 { ballarin@24087 619 assume "x \ y" ballarin@24087 620 with L have "least L y (Upper L {x, y})" ballarin@24087 621 by (rule_tac least_UpperI) auto ballarin@24087 622 } ballarin@24087 623 moreover ballarin@24087 624 { ballarin@24087 625 assume "y \ x" ballarin@24087 626 with L have "least L x (Upper L {x, y})" ballarin@24087 627 by (rule_tac least_UpperI) auto ballarin@24087 628 } ballarin@24087 629 ultimately show ?thesis by blast ballarin@14551 630 qed ballarin@24087 631 next ballarin@24087 632 fix x y ballarin@24087 633 assume L: "x \ carrier L" "y \ carrier L" wenzelm@67091 634 show "\i. greatest L i (Lower L {x, y})" ballarin@24087 635 proof - ballarin@24087 636 note total L ballarin@24087 637 moreover ballarin@24087 638 { ballarin@24087 639 assume "y \ x" ballarin@24087 640 with L have "greatest L y (Lower L {x, y})" ballarin@24087 641 by (rule_tac greatest_LowerI) auto ballarin@24087 642 } ballarin@24087 643 moreover ballarin@24087 644 { ballarin@24087 645 assume "x \ y" ballarin@24087 646 with L have "greatest L x (Lower L {x, y})" ballarin@24087 647 by (rule_tac greatest_LowerI) auto ballarin@24087 648 } ballarin@24087 649 ultimately show ?thesis by blast ballarin@24087 650 qed ballarin@24087 651 qed ballarin@14551 652 wenzelm@14693 653 ballarin@65099 654 subsection \Weak Bounded Lattices\ ballarin@14551 655 ballarin@65099 656 locale weak_bounded_lattice = ballarin@65099 657 weak_lattice + ballarin@65099 658 weak_partial_order_bottom + ballarin@65099 659 weak_partial_order_top ballarin@27713 660 begin ballarin@27713 661 ballarin@65099 662 lemma bottom_meet: "x \ carrier L \ \ \ x .= \" ballarin@65099 663 by (metis bottom_least least_def meet_closed meet_left weak_le_antisym) ballarin@27713 664 ballarin@65099 665 lemma bottom_join: "x \ carrier L \ \ \ x .= x" ballarin@65099 666 by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym) ballarin@27713 667 ballarin@65099 668 lemma bottom_weak_eq: ballarin@65099 669 "\ b \ carrier L; \ x. x \ carrier L \ b \ x \ \ b .= \" ballarin@65099 670 by (metis bottom_closed bottom_lower weak_le_antisym) ballarin@27713 671 ballarin@65099 672 lemma top_join: "x \ carrier L \ \ \ x .= \" ballarin@65099 673 by (metis join_closed join_left top_closed top_higher weak_le_antisym) ballarin@65099 674 ballarin@65099 675 lemma top_meet: "x \ carrier L \ \ \ x .= x" ballarin@65099 676 by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym) ballarin@65099 677 ballarin@65099 678 lemma top_weak_eq: "\ t \ carrier L; \ x. x \ carrier L \ x \ t \ \ t .= \" ballarin@65099 679 by (metis top_closed top_higher weak_le_antisym) ballarin@27713 680 ballarin@27713 681 end ballarin@27713 682 ballarin@65099 683 sublocale weak_bounded_lattice \ weak_partial_order .. ballarin@27713 684 ballarin@27713 685 ballarin@65099 686 subsection \Lattices where \eq\ is the Equality\ ballarin@27713 687 ballarin@27713 688 locale upper_semilattice = partial_order + ballarin@27713 689 assumes sup_of_two_exists: wenzelm@67091 690 "[| x \ carrier L; y \ carrier L |] ==> \s. least L s (Upper L {x, y})" ballarin@27713 691 ballarin@65099 692 sublocale upper_semilattice \ weak?: weak_upper_semilattice ballarin@65099 693 by unfold_locales (rule sup_of_two_exists) ballarin@27713 694 ballarin@27713 695 locale lower_semilattice = partial_order + ballarin@27713 696 assumes inf_of_two_exists: wenzelm@67091 697 "[| x \ carrier L; y \ carrier L |] ==> \s. greatest L s (Lower L {x, y})" ballarin@27713 698 ballarin@65099 699 sublocale lower_semilattice \ weak?: weak_lower_semilattice ballarin@65099 700 by unfold_locales (rule inf_of_two_exists) ballarin@27713 701 ballarin@27713 702 locale lattice = upper_semilattice + lower_semilattice ballarin@27713 703 ballarin@65099 704 sublocale lattice \ weak_lattice .. ballarin@27713 705 ballarin@65099 706 lemma (in lattice) dual_lattice: ballarin@65099 707 "lattice (inv_gorder L)" ballarin@65099 708 proof - ballarin@65099 709 interpret dual: weak_lattice "inv_gorder L" ballarin@65099 710 by (metis dual_weak_lattice) ballarin@27713 711 ballarin@65099 712 show ?thesis ballarin@65099 713 apply (unfold_locales) ballarin@65099 714 apply (simp_all add: inf_of_two_exists sup_of_two_exists) ballarin@65099 715 apply (simp add:eq_is_equal) ballarin@65099 716 done ballarin@65099 717 qed ballarin@65099 718 ballarin@65099 719 lemma (in lattice) le_iff_join: ballarin@65099 720 assumes "x \ carrier L" "y \ carrier L" ballarin@65099 721 shows "x \ y \ x = (x \ y)" ballarin@65099 722 by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join) ballarin@27713 723 ballarin@65099 724 lemma (in lattice) le_iff_meet: ballarin@65099 725 assumes "x \ carrier L" "y \ carrier L" ballarin@65099 726 shows "x \ y \ (x \ y) = y" ballarin@65099 727 by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet) ballarin@27713 728 ballarin@65099 729 text \ Total orders are lattices. \ ballarin@27713 730 ballarin@65099 731 sublocale total_order \ weak?: lattice ballarin@65099 732 by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists) ballarin@65099 733 ballarin@65099 734 text \Functions that preserve joins and meets\ ballarin@65099 735 ballarin@65099 736 definition join_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where ballarin@65099 737 "join_pres X Y f \ lattice X \ lattice Y \ (\ x \ carrier X. \ y \ carrier X. f (x \\<^bsub>X\<^esub> y) = f x \\<^bsub>Y\<^esub> f y)" ballarin@27713 738 ballarin@65099 739 definition meet_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where ballarin@65099 740 "meet_pres X Y f \ lattice X \ lattice Y \ (\ x \ carrier X. \ y \ carrier X. f (x \\<^bsub>X\<^esub> y) = f x \\<^bsub>Y\<^esub> f y)" ballarin@27713 741 ballarin@65099 742 lemma join_pres_isotone: ballarin@65099 743 assumes "f \ carrier X \ carrier Y" "join_pres X Y f" ballarin@65099 744 shows "isotone X Y f" ballarin@65099 745 using assms ballarin@65099 746 apply (rule_tac isotoneI) ballarin@65099 747 apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier) ballarin@65099 748 using lattice_def partial_order_def upper_semilattice_def apply blast ballarin@65099 749 using lattice_def partial_order_def upper_semilattice_def apply blast ballarin@65099 750 apply fastforce ballarin@65099 751 done ballarin@27713 752 ballarin@65099 753 lemma meet_pres_isotone: ballarin@65099 754 assumes "f \ carrier X \ carrier Y" "meet_pres X Y f" ballarin@65099 755 shows "isotone X Y f" ballarin@65099 756 using assms ballarin@65099 757 apply (rule_tac isotoneI) ballarin@65099 758 apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier) ballarin@65099 759 using lattice_def partial_order_def upper_semilattice_def apply blast ballarin@65099 760 using lattice_def partial_order_def upper_semilattice_def apply blast ballarin@65099 761 apply fastforce ballarin@65099 762 done ballarin@27713 763 ballarin@27713 764 ballarin@65099 765 subsection \Bounded Lattices\ ballarin@27713 766 ballarin@65099 767 locale bounded_lattice = ballarin@65099 768 lattice + ballarin@65099 769 weak_partial_order_bottom + ballarin@65099 770 weak_partial_order_top ballarin@27713 771 ballarin@65099 772 sublocale bounded_lattice \ weak_bounded_lattice .. ballarin@27713 773 ballarin@65099 774 context bounded_lattice ballarin@65099 775 begin ballarin@14551 776 ballarin@65099 777 lemma bottom_eq: ballarin@65099 778 "\ b \ carrier L; \ x. x \ carrier L \ b \ x \ \ b = \" ballarin@65099 779 by (metis bottom_closed bottom_lower le_antisym) ballarin@14551 780 ballarin@65099 781 lemma top_eq: "\ t \ carrier L; \ x. x \ carrier L \ x \ t \ \ t = \" ballarin@65099 782 by (metis le_antisym top_closed top_higher) ballarin@14551 783 wenzelm@14693 784 end ballarin@65099 785 ballarin@65099 786 end