summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/Lattice.thy

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 16417 | 9bc16273c2d4 |

child 19286 | 83404ccd270a |

permissions | -rw-r--r-- |

Constant "If" is now local

1 (*

2 Title: HOL/Algebra/Lattice.thy

3 Id: $Id$

4 Author: Clemens Ballarin, started 7 November 2003

5 Copyright: Clemens Ballarin

6 *)

8 header {* Orders and Lattices *}

10 theory Lattice imports Main begin

12 text {* Object with a carrier set. *}

14 record 'a partial_object =

15 carrier :: "'a set"

17 subsection {* Partial Orders *}

19 record 'a order = "'a partial_object" +

20 le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)

22 locale partial_order = struct L +

23 assumes refl [intro, simp]:

24 "x \<in> carrier L ==> x \<sqsubseteq> x"

25 and anti_sym [intro]:

26 "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"

27 and trans [trans]:

28 "[| x \<sqsubseteq> y; y \<sqsubseteq> z;

29 x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"

31 constdefs (structure L)

32 less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)

33 "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"

35 -- {* Upper and lower bounds of a set. *}

36 Upper :: "[_, 'a set] => 'a set"

37 "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>

38 carrier L"

40 Lower :: "[_, 'a set] => 'a set"

41 "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>

42 carrier L"

44 -- {* Least and greatest, as predicate. *}

45 least :: "[_, 'a, 'a set] => bool"

46 "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"

48 greatest :: "[_, 'a, 'a set] => bool"

49 "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"

51 -- {* Supremum and infimum *}

52 sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)

53 "\<Squnion>A == THE x. least L x (Upper L A)"

55 inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)

56 "\<Sqinter>A == THE x. greatest L x (Lower L A)"

58 join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)

59 "x \<squnion> y == sup L {x, y}"

61 meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)

62 "x \<sqinter> y == inf L {x, y}"

65 subsubsection {* Upper *}

67 lemma Upper_closed [intro, simp]:

68 "Upper L A \<subseteq> carrier L"

69 by (unfold Upper_def) clarify

71 lemma UpperD [dest]:

72 includes struct L

73 shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"

74 by (unfold Upper_def) blast

76 lemma Upper_memI:

77 includes struct L

78 shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"

79 by (unfold Upper_def) blast

81 lemma Upper_antimono:

82 "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"

83 by (unfold Upper_def) blast

86 subsubsection {* Lower *}

88 lemma Lower_closed [intro, simp]:

89 "Lower L A \<subseteq> carrier L"

90 by (unfold Lower_def) clarify

92 lemma LowerD [dest]:

93 includes struct L

94 shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"

95 by (unfold Lower_def) blast

97 lemma Lower_memI:

98 includes struct L

99 shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"

100 by (unfold Lower_def) blast

102 lemma Lower_antimono:

103 "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"

104 by (unfold Lower_def) blast

107 subsubsection {* least *}

109 lemma least_carrier [intro, simp]:

110 shows "least L l A ==> l \<in> carrier L"

111 by (unfold least_def) fast

113 lemma least_mem:

114 "least L l A ==> l \<in> A"

115 by (unfold least_def) fast

117 lemma (in partial_order) least_unique:

118 "[| least L x A; least L y A |] ==> x = y"

119 by (unfold least_def) blast

121 lemma least_le:

122 includes struct L

123 shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"

124 by (unfold least_def) fast

126 lemma least_UpperI:

127 includes struct L

128 assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"

129 and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"

130 and L: "A \<subseteq> carrier L" "s \<in> carrier L"

131 shows "least L s (Upper L A)"

132 proof -

133 have "Upper L A \<subseteq> carrier L" by simp

134 moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)

135 moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast

136 ultimately show ?thesis by (simp add: least_def)

137 qed

140 subsubsection {* greatest *}

142 lemma greatest_carrier [intro, simp]:

143 shows "greatest L l A ==> l \<in> carrier L"

144 by (unfold greatest_def) fast

146 lemma greatest_mem:

147 "greatest L l A ==> l \<in> A"

148 by (unfold greatest_def) fast

150 lemma (in partial_order) greatest_unique:

151 "[| greatest L x A; greatest L y A |] ==> x = y"

152 by (unfold greatest_def) blast

154 lemma greatest_le:

155 includes struct L

156 shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"

157 by (unfold greatest_def) fast

159 lemma greatest_LowerI:

160 includes struct L

161 assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"

162 and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"

163 and L: "A \<subseteq> carrier L" "i \<in> carrier L"

164 shows "greatest L i (Lower L A)"

165 proof -

166 have "Lower L A \<subseteq> carrier L" by simp

167 moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)

168 moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast

169 ultimately show ?thesis by (simp add: greatest_def)

170 qed

173 subsection {* Lattices *}

175 locale lattice = partial_order +

176 assumes sup_of_two_exists:

177 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"

178 and inf_of_two_exists:

179 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"

181 lemma least_Upper_above:

182 includes struct L

183 shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"

184 by (unfold least_def) blast

186 lemma greatest_Lower_above:

187 includes struct L

188 shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"

189 by (unfold greatest_def) blast

192 subsubsection {* Supremum *}

194 lemma (in lattice) joinI:

195 "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]

196 ==> P (x \<squnion> y)"

197 proof (unfold join_def sup_def)

198 assume L: "x \<in> carrier L" "y \<in> carrier L"

199 and P: "!!l. least L l (Upper L {x, y}) ==> P l"

200 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast

201 with L show "P (THE l. least L l (Upper L {x, y}))"

202 by (fast intro: theI2 least_unique P)

203 qed

205 lemma (in lattice) join_closed [simp]:

206 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"

207 by (rule joinI) (rule least_carrier)

209 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *)

210 "x \<in> carrier L ==> least L x (Upper L {x})"

211 by (rule least_UpperI) fast+

213 lemma (in partial_order) sup_of_singleton [simp]:

214 includes struct L

215 shows "x \<in> carrier L ==> \<Squnion>{x} = x"

216 by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)

219 text {* Condition on @{text A}: supremum exists. *}

221 lemma (in lattice) sup_insertI:

222 "[| !!s. least L s (Upper L (insert x A)) ==> P s;

223 least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]

224 ==> P (\<Squnion>(insert x A))"

225 proof (unfold sup_def)

226 assume L: "x \<in> carrier L" "A \<subseteq> carrier L"

227 and P: "!!l. least L l (Upper L (insert x A)) ==> P l"

228 and least_a: "least L a (Upper L A)"

229 from L least_a have La: "a \<in> carrier L" by simp

230 from L sup_of_two_exists least_a

231 obtain s where least_s: "least L s (Upper L {a, x})" by blast

232 show "P (THE l. least L l (Upper L (insert x A)))"

233 proof (rule theI2)

234 show "least L s (Upper L (insert x A))"

235 proof (rule least_UpperI)

236 fix z

237 assume "z \<in> insert x A"

238 then show "z \<sqsubseteq> s"

239 proof

240 assume "z = x" then show ?thesis

241 by (simp add: least_Upper_above [OF least_s] L La)

242 next

243 assume "z \<in> A"

244 with L least_s least_a show ?thesis

245 by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)

246 qed

247 next

248 fix y

249 assume y: "y \<in> Upper L (insert x A)"

250 show "s \<sqsubseteq> y"

251 proof (rule least_le [OF least_s], rule Upper_memI)

252 fix z

253 assume z: "z \<in> {a, x}"

254 then show "z \<sqsubseteq> y"

255 proof

256 have y': "y \<in> Upper L A"

257 apply (rule subsetD [where A = "Upper L (insert x A)"])

258 apply (rule Upper_antimono) apply clarify apply assumption

259 done

260 assume "z = a"

261 with y' least_a show ?thesis by (fast dest: least_le)

262 next

263 assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)

264 with y L show ?thesis by blast

265 qed

266 qed (rule Upper_closed [THEN subsetD])

267 next

268 from L show "insert x A \<subseteq> carrier L" by simp

269 from least_s show "s \<in> carrier L" by simp

270 qed

271 next

272 fix l

273 assume least_l: "least L l (Upper L (insert x A))"

274 show "l = s"

275 proof (rule least_unique)

276 show "least L s (Upper L (insert x A))"

277 proof (rule least_UpperI)

278 fix z

279 assume "z \<in> insert x A"

280 then show "z \<sqsubseteq> s"

281 proof

282 assume "z = x" then show ?thesis

283 by (simp add: least_Upper_above [OF least_s] L La)

284 next

285 assume "z \<in> A"

286 with L least_s least_a show ?thesis

287 by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)

288 qed

289 next

290 fix y

291 assume y: "y \<in> Upper L (insert x A)"

292 show "s \<sqsubseteq> y"

293 proof (rule least_le [OF least_s], rule Upper_memI)

294 fix z

295 assume z: "z \<in> {a, x}"

296 then show "z \<sqsubseteq> y"

297 proof

298 have y': "y \<in> Upper L A"

299 apply (rule subsetD [where A = "Upper L (insert x A)"])

300 apply (rule Upper_antimono) apply clarify apply assumption

301 done

302 assume "z = a"

303 with y' least_a show ?thesis by (fast dest: least_le)

304 next

305 assume "z \<in> {x}"

306 with y L show ?thesis by blast

307 qed

308 qed (rule Upper_closed [THEN subsetD])

309 next

310 from L show "insert x A \<subseteq> carrier L" by simp

311 from least_s show "s \<in> carrier L" by simp

312 qed

313 qed

314 qed

315 qed

317 lemma (in lattice) finite_sup_least:

318 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"

319 proof (induct set: Finites)

320 case empty

321 then show ?case by simp

322 next

323 case (insert x A)

324 show ?case

325 proof (cases "A = {}")

326 case True

327 with insert show ?thesis by (simp add: sup_of_singletonI)

328 next

329 case False

330 with insert have "least L (\<Squnion>A) (Upper L A)" by simp

331 with _ show ?thesis

332 by (rule sup_insertI) (simp_all add: insert [simplified])

333 qed

334 qed

336 lemma (in lattice) finite_sup_insertI:

337 assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"

338 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"

339 shows "P (\<Squnion> (insert x A))"

340 proof (cases "A = {}")

341 case True with P and xA show ?thesis

342 by (simp add: sup_of_singletonI)

343 next

344 case False with P and xA show ?thesis

345 by (simp add: sup_insertI finite_sup_least)

346 qed

348 lemma (in lattice) finite_sup_closed:

349 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"

350 proof (induct set: Finites)

351 case empty then show ?case by simp

352 next

353 case insert then show ?case

354 by - (rule finite_sup_insertI, simp_all)

355 qed

357 lemma (in lattice) join_left:

358 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"

359 by (rule joinI [folded join_def]) (blast dest: least_mem)

361 lemma (in lattice) join_right:

362 "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"

363 by (rule joinI [folded join_def]) (blast dest: least_mem)

365 lemma (in lattice) sup_of_two_least:

366 "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"

367 proof (unfold sup_def)

368 assume L: "x \<in> carrier L" "y \<in> carrier L"

369 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast

370 with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"

371 by (fast intro: theI2 least_unique) (* blast fails *)

372 qed

374 lemma (in lattice) join_le:

375 assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z"

376 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"

377 shows "x \<squnion> y \<sqsubseteq> z"

378 proof (rule joinI)

379 fix s

380 assume "least L s (Upper L {x, y})"

381 with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)

382 qed

384 lemma (in lattice) join_assoc_lemma:

385 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"

386 shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"

387 proof (rule finite_sup_insertI)

388 -- {* The textbook argument in Jacobson I, p 457 *}

389 fix s

390 assume sup: "least L s (Upper L {x, y, z})"

391 show "x \<squnion> (y \<squnion> z) = s"

392 proof (rule anti_sym)

393 from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"

394 by (fastsimp intro!: join_le elim: least_Upper_above)

395 next

396 from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"

397 by (erule_tac least_le)

398 (blast intro!: Upper_memI intro: trans join_left join_right join_closed)

399 qed (simp_all add: L least_carrier [OF sup])

400 qed (simp_all add: L)

402 lemma join_comm:

403 includes struct L

404 shows "x \<squnion> y = y \<squnion> x"

405 by (unfold join_def) (simp add: insert_commute)

407 lemma (in lattice) join_assoc:

408 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"

409 shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"

410 proof -

411 have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)

412 also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)

413 also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)

414 also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)

415 finally show ?thesis .

416 qed

419 subsubsection {* Infimum *}

421 lemma (in lattice) meetI:

422 "[| !!i. greatest L i (Lower L {x, y}) ==> P i;

423 x \<in> carrier L; y \<in> carrier L |]

424 ==> P (x \<sqinter> y)"

425 proof (unfold meet_def inf_def)

426 assume L: "x \<in> carrier L" "y \<in> carrier L"

427 and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"

428 with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast

429 with L show "P (THE g. greatest L g (Lower L {x, y}))"

430 by (fast intro: theI2 greatest_unique P)

431 qed

433 lemma (in lattice) meet_closed [simp]:

434 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"

435 by (rule meetI) (rule greatest_carrier)

437 lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *)

438 "x \<in> carrier L ==> greatest L x (Lower L {x})"

439 by (rule greatest_LowerI) fast+

441 lemma (in partial_order) inf_of_singleton [simp]:

442 includes struct L

443 shows "x \<in> carrier L ==> \<Sqinter> {x} = x"

444 by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)

446 text {* Condition on A: infimum exists. *}

448 lemma (in lattice) inf_insertI:

449 "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;

450 greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]

451 ==> P (\<Sqinter>(insert x A))"

452 proof (unfold inf_def)

453 assume L: "x \<in> carrier L" "A \<subseteq> carrier L"

454 and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"

455 and greatest_a: "greatest L a (Lower L A)"

456 from L greatest_a have La: "a \<in> carrier L" by simp

457 from L inf_of_two_exists greatest_a

458 obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast

459 show "P (THE g. greatest L g (Lower L (insert x A)))"

460 proof (rule theI2)

461 show "greatest L i (Lower L (insert x A))"

462 proof (rule greatest_LowerI)

463 fix z

464 assume "z \<in> insert x A"

465 then show "i \<sqsubseteq> z"

466 proof

467 assume "z = x" then show ?thesis

468 by (simp add: greatest_Lower_above [OF greatest_i] L La)

469 next

470 assume "z \<in> A"

471 with L greatest_i greatest_a show ?thesis

472 by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)

473 qed

474 next

475 fix y

476 assume y: "y \<in> Lower L (insert x A)"

477 show "y \<sqsubseteq> i"

478 proof (rule greatest_le [OF greatest_i], rule Lower_memI)

479 fix z

480 assume z: "z \<in> {a, x}"

481 then show "y \<sqsubseteq> z"

482 proof

483 have y': "y \<in> Lower L A"

484 apply (rule subsetD [where A = "Lower L (insert x A)"])

485 apply (rule Lower_antimono) apply clarify apply assumption

486 done

487 assume "z = a"

488 with y' greatest_a show ?thesis by (fast dest: greatest_le)

489 next

490 assume "z \<in> {x}"

491 with y L show ?thesis by blast

492 qed

493 qed (rule Lower_closed [THEN subsetD])

494 next

495 from L show "insert x A \<subseteq> carrier L" by simp

496 from greatest_i show "i \<in> carrier L" by simp

497 qed

498 next

499 fix g

500 assume greatest_g: "greatest L g (Lower L (insert x A))"

501 show "g = i"

502 proof (rule greatest_unique)

503 show "greatest L i (Lower L (insert x A))"

504 proof (rule greatest_LowerI)

505 fix z

506 assume "z \<in> insert x A"

507 then show "i \<sqsubseteq> z"

508 proof

509 assume "z = x" then show ?thesis

510 by (simp add: greatest_Lower_above [OF greatest_i] L La)

511 next

512 assume "z \<in> A"

513 with L greatest_i greatest_a show ?thesis

514 by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)

515 qed

516 next

517 fix y

518 assume y: "y \<in> Lower L (insert x A)"

519 show "y \<sqsubseteq> i"

520 proof (rule greatest_le [OF greatest_i], rule Lower_memI)

521 fix z

522 assume z: "z \<in> {a, x}"

523 then show "y \<sqsubseteq> z"

524 proof

525 have y': "y \<in> Lower L A"

526 apply (rule subsetD [where A = "Lower L (insert x A)"])

527 apply (rule Lower_antimono) apply clarify apply assumption

528 done

529 assume "z = a"

530 with y' greatest_a show ?thesis by (fast dest: greatest_le)

531 next

532 assume "z \<in> {x}"

533 with y L show ?thesis by blast

534 qed

535 qed (rule Lower_closed [THEN subsetD])

536 next

537 from L show "insert x A \<subseteq> carrier L" by simp

538 from greatest_i show "i \<in> carrier L" by simp

539 qed

540 qed

541 qed

542 qed

544 lemma (in lattice) finite_inf_greatest:

545 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"

546 proof (induct set: Finites)

547 case empty then show ?case by simp

548 next

549 case (insert x A)

550 show ?case

551 proof (cases "A = {}")

552 case True

553 with insert show ?thesis by (simp add: inf_of_singletonI)

554 next

555 case False

556 from insert show ?thesis

557 proof (rule_tac inf_insertI)

558 from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp

559 qed simp_all

560 qed

561 qed

563 lemma (in lattice) finite_inf_insertI:

564 assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"

565 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"

566 shows "P (\<Sqinter> (insert x A))"

567 proof (cases "A = {}")

568 case True with P and xA show ?thesis

569 by (simp add: inf_of_singletonI)

570 next

571 case False with P and xA show ?thesis

572 by (simp add: inf_insertI finite_inf_greatest)

573 qed

575 lemma (in lattice) finite_inf_closed:

576 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"

577 proof (induct set: Finites)

578 case empty then show ?case by simp

579 next

580 case insert then show ?case

581 by (rule_tac finite_inf_insertI) (simp_all)

582 qed

584 lemma (in lattice) meet_left:

585 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"

586 by (rule meetI [folded meet_def]) (blast dest: greatest_mem)

588 lemma (in lattice) meet_right:

589 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"

590 by (rule meetI [folded meet_def]) (blast dest: greatest_mem)

592 lemma (in lattice) inf_of_two_greatest:

593 "[| x \<in> carrier L; y \<in> carrier L |] ==>

594 greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"

595 proof (unfold inf_def)

596 assume L: "x \<in> carrier L" "y \<in> carrier L"

597 with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast

598 with L

599 show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"

600 by (fast intro: theI2 greatest_unique) (* blast fails *)

601 qed

603 lemma (in lattice) meet_le:

604 assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y"

605 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"

606 shows "z \<sqsubseteq> x \<sqinter> y"

607 proof (rule meetI)

608 fix i

609 assume "greatest L i (Lower L {x, y})"

610 with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)

611 qed

613 lemma (in lattice) meet_assoc_lemma:

614 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"

615 shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"

616 proof (rule finite_inf_insertI)

617 txt {* The textbook argument in Jacobson I, p 457 *}

618 fix i

619 assume inf: "greatest L i (Lower L {x, y, z})"

620 show "x \<sqinter> (y \<sqinter> z) = i"

621 proof (rule anti_sym)

622 from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"

623 by (fastsimp intro!: meet_le elim: greatest_Lower_above)

624 next

625 from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"

626 by (erule_tac greatest_le)

627 (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)

628 qed (simp_all add: L greatest_carrier [OF inf])

629 qed (simp_all add: L)

631 lemma meet_comm:

632 includes struct L

633 shows "x \<sqinter> y = y \<sqinter> x"

634 by (unfold meet_def) (simp add: insert_commute)

636 lemma (in lattice) meet_assoc:

637 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"

638 shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"

639 proof -

640 have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)

641 also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma)

642 also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)

643 also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma)

644 finally show ?thesis .

645 qed

648 subsection {* Total Orders *}

650 locale total_order = lattice +

651 assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"

653 text {* Introduction rule: the usual definition of total order *}

655 lemma (in partial_order) total_orderI:

656 assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"

657 shows "total_order L"

658 proof (rule total_order.intro)

659 show "lattice_axioms L"

660 proof (rule lattice_axioms.intro)

661 fix x y

662 assume L: "x \<in> carrier L" "y \<in> carrier L"

663 show "EX s. least L s (Upper L {x, y})"

664 proof -

665 note total L

666 moreover

667 {

668 assume "x \<sqsubseteq> y"

669 with L have "least L y (Upper L {x, y})"

670 by (rule_tac least_UpperI) auto

671 }

672 moreover

673 {

674 assume "y \<sqsubseteq> x"

675 with L have "least L x (Upper L {x, y})"

676 by (rule_tac least_UpperI) auto

677 }

678 ultimately show ?thesis by blast

679 qed

680 next

681 fix x y

682 assume L: "x \<in> carrier L" "y \<in> carrier L"

683 show "EX i. greatest L i (Lower L {x, y})"

684 proof -

685 note total L

686 moreover

687 {

688 assume "y \<sqsubseteq> x"

689 with L have "greatest L y (Lower L {x, y})"

690 by (rule_tac greatest_LowerI) auto

691 }

692 moreover

693 {

694 assume "x \<sqsubseteq> y"

695 with L have "greatest L x (Lower L {x, y})"

696 by (rule_tac greatest_LowerI) auto

697 }

698 ultimately show ?thesis by blast

699 qed

700 qed

701 qed (assumption | rule total_order_axioms.intro)+

704 subsection {* Complete lattices *}

706 locale complete_lattice = lattice +

707 assumes sup_exists:

708 "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"

709 and inf_exists:

710 "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"

712 text {* Introduction rule: the usual definition of complete lattice *}

714 lemma (in partial_order) complete_latticeI:

715 assumes sup_exists:

716 "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"

717 and inf_exists:

718 "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"

719 shows "complete_lattice L"

720 proof (rule complete_lattice.intro)

721 show "lattice_axioms L"

722 by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+

723 qed (assumption | rule complete_lattice_axioms.intro)+

725 constdefs (structure L)

726 top :: "_ => 'a" ("\<top>\<index>")

727 "\<top> == sup L (carrier L)"

729 bottom :: "_ => 'a" ("\<bottom>\<index>")

730 "\<bottom> == inf L (carrier L)"

733 lemma (in complete_lattice) supI:

734 "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]

735 ==> P (\<Squnion>A)"

736 proof (unfold sup_def)

737 assume L: "A \<subseteq> carrier L"

738 and P: "!!l. least L l (Upper L A) ==> P l"

739 with sup_exists obtain s where "least L s (Upper L A)" by blast

740 with L show "P (THE l. least L l (Upper L A))"

741 by (fast intro: theI2 least_unique P)

742 qed

744 lemma (in complete_lattice) sup_closed [simp]:

745 "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"

746 by (rule supI) simp_all

748 lemma (in complete_lattice) top_closed [simp, intro]:

749 "\<top> \<in> carrier L"

750 by (unfold top_def) simp

752 lemma (in complete_lattice) infI:

753 "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]

754 ==> P (\<Sqinter>A)"

755 proof (unfold inf_def)

756 assume L: "A \<subseteq> carrier L"

757 and P: "!!l. greatest L l (Lower L A) ==> P l"

758 with inf_exists obtain s where "greatest L s (Lower L A)" by blast

759 with L show "P (THE l. greatest L l (Lower L A))"

760 by (fast intro: theI2 greatest_unique P)

761 qed

763 lemma (in complete_lattice) inf_closed [simp]:

764 "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"

765 by (rule infI) simp_all

767 lemma (in complete_lattice) bottom_closed [simp, intro]:

768 "\<bottom> \<in> carrier L"

769 by (unfold bottom_def) simp

771 text {* Jacobson: Theorem 8.1 *}

773 lemma Lower_empty [simp]:

774 "Lower L {} = carrier L"

775 by (unfold Lower_def) simp

777 lemma Upper_empty [simp]:

778 "Upper L {} = carrier L"

779 by (unfold Upper_def) simp

781 theorem (in partial_order) complete_lattice_criterion1:

782 assumes top_exists: "EX g. greatest L g (carrier L)"

783 and inf_exists:

784 "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"

785 shows "complete_lattice L"

786 proof (rule complete_latticeI)

787 from top_exists obtain top where top: "greatest L top (carrier L)" ..

788 fix A

789 assume L: "A \<subseteq> carrier L"

790 let ?B = "Upper L A"

791 from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)

792 then have B_non_empty: "?B ~= {}" by fast

793 have B_L: "?B \<subseteq> carrier L" by simp

794 from inf_exists [OF B_L B_non_empty]

795 obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..

796 have "least L b (Upper L A)"

797 apply (rule least_UpperI)

798 apply (rule greatest_le [where A = "Lower L ?B"])

799 apply (rule b_inf_B)

800 apply (rule Lower_memI)

801 apply (erule UpperD)

802 apply assumption

803 apply (rule L)

804 apply (fast intro: L [THEN subsetD])

805 apply (erule greatest_Lower_above [OF b_inf_B])

806 apply simp

807 apply (rule L)

808 apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)

809 done

810 then show "EX s. least L s (Upper L A)" ..

811 next

812 fix A

813 assume L: "A \<subseteq> carrier L"

814 show "EX i. greatest L i (Lower L A)"

815 proof (cases "A = {}")

816 case True then show ?thesis

817 by (simp add: top_exists)

818 next

819 case False with L show ?thesis

820 by (rule inf_exists)

821 qed

822 qed

824 (* TODO: prove dual version *)

826 subsection {* Examples *}

828 subsubsection {* Powerset of a set is a complete lattice *}

830 theorem powerset_is_complete_lattice:

831 "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"

832 (is "complete_lattice ?L")

833 proof (rule partial_order.complete_latticeI)

834 show "partial_order ?L"

835 by (rule partial_order.intro) auto

836 next

837 fix B

838 assume "B \<subseteq> carrier ?L"

839 then have "least ?L (\<Union> B) (Upper ?L B)"

840 by (fastsimp intro!: least_UpperI simp: Upper_def)

841 then show "EX s. least ?L s (Upper ?L B)" ..

842 next

843 fix B

844 assume "B \<subseteq> carrier ?L"

845 then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"

846 txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:

847 @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}

848 by (fastsimp intro!: greatest_LowerI simp: Lower_def)

849 then show "EX i. greatest ?L i (Lower ?L B)" ..

850 qed

852 text {* An other example, that of the lattice of subgroups of a group,

853 can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}

855 end