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

src/HOL/Algebra/Lattice.thy

author | haftmann |

Fri Apr 20 11:21:42 2007 +0200 (2007-04-20) | |

changeset 22744 | 5cbe966d67a2 |

parent 22265 | 3c5c6bdf61de |

child 23350 | 50c5b0912a0c |

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

Isar definitions are now added explicitly to code theorem table

1 (*

2 Title: HOL/Algebra/Lattice.thy

3 Id: $Id$

4 Author: Clemens Ballarin, started 7 November 2003

5 Copyright: Clemens Ballarin

6 *)

8 theory Lattice imports Main begin

11 section {* Orders and Lattices *}

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

15 record 'a partial_object =

16 carrier :: "'a set"

19 subsection {* Partial Orders *}

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

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

24 locale partial_order =

25 fixes L (structure)

26 assumes refl [intro, simp]:

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

28 and anti_sym [intro]:

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

30 and trans [trans]:

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

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

34 constdefs (structure L)

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

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

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

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

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

41 carrier L"

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

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

45 carrier L"

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

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

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

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

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

54 -- {* Supremum and infimum *}

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

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

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

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

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

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

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

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

68 subsubsection {* Upper *}

70 lemma Upper_closed [intro, simp]:

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

72 by (unfold Upper_def) clarify

74 lemma UpperD [dest]:

75 fixes L (structure)

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

77 by (unfold Upper_def) blast

79 lemma Upper_memI:

80 fixes L (structure)

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

82 by (unfold Upper_def) blast

84 lemma Upper_antimono:

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

86 by (unfold Upper_def) blast

89 subsubsection {* Lower *}

91 lemma Lower_closed [intro, simp]:

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

93 by (unfold Lower_def) clarify

95 lemma LowerD [dest]:

96 fixes L (structure)

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

98 by (unfold Lower_def) blast

100 lemma Lower_memI:

101 fixes L (structure)

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

103 by (unfold Lower_def) blast

105 lemma Lower_antimono:

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

107 by (unfold Lower_def) blast

110 subsubsection {* least *}

112 lemma least_carrier [intro, simp]:

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

114 by (unfold least_def) fast

116 lemma least_mem:

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

118 by (unfold least_def) fast

120 lemma (in partial_order) least_unique:

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

122 by (unfold least_def) blast

124 lemma least_le:

125 fixes L (structure)

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

127 by (unfold least_def) fast

129 lemma least_UpperI:

130 fixes L (structure)

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

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

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

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

135 proof -

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

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

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

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

140 qed

143 subsubsection {* greatest *}

145 lemma greatest_carrier [intro, simp]:

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

147 by (unfold greatest_def) fast

149 lemma greatest_mem:

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

151 by (unfold greatest_def) fast

153 lemma (in partial_order) greatest_unique:

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

155 by (unfold greatest_def) blast

157 lemma greatest_le:

158 fixes L (structure)

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

160 by (unfold greatest_def) fast

162 lemma greatest_LowerI:

163 fixes L (structure)

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

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

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

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

168 proof -

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

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

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

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

173 qed

176 subsection {* Lattices *}

178 locale lattice = partial_order +

179 assumes sup_of_two_exists:

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

181 and inf_of_two_exists:

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

184 lemma least_Upper_above:

185 fixes L (structure)

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

187 by (unfold least_def) blast

189 lemma greatest_Lower_above:

190 fixes L (structure)

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

192 by (unfold greatest_def) blast

195 subsubsection {* Supremum *}

197 lemma (in lattice) joinI:

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

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

200 proof (unfold join_def sup_def)

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

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

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

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

205 by (fast intro: theI2 least_unique P)

206 qed

208 lemma (in lattice) join_closed [simp]:

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

210 by (rule joinI) (rule least_carrier)

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

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

214 by (rule least_UpperI) fast+

216 lemma (in partial_order) sup_of_singleton [simp]:

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

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

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

223 lemma (in lattice) sup_insertI:

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

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

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

227 proof (unfold sup_def)

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

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

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

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

232 from L sup_of_two_exists least_a

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

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

235 proof (rule theI2)

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

237 proof (rule least_UpperI)

238 fix z

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

240 then show "z \<sqsubseteq> s"

241 proof

242 assume "z = x" then show ?thesis

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

244 next

245 assume "z \<in> A"

246 with L least_s least_a show ?thesis

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

248 qed

249 next

250 fix y

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

252 show "s \<sqsubseteq> y"

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

254 fix z

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

256 then show "z \<sqsubseteq> y"

257 proof

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

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

260 apply (rule Upper_antimono) apply clarify apply assumption

261 done

262 assume "z = a"

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

264 next

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

266 with y L show ?thesis by blast

267 qed

268 qed (rule Upper_closed [THEN subsetD])

269 next

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

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

272 qed

273 next

274 fix l

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

276 show "l = s"

277 proof (rule least_unique)

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

279 proof (rule least_UpperI)

280 fix z

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

282 then show "z \<sqsubseteq> s"

283 proof

284 assume "z = x" then show ?thesis

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

286 next

287 assume "z \<in> A"

288 with L least_s least_a show ?thesis

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

290 qed

291 next

292 fix y

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

294 show "s \<sqsubseteq> y"

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

296 fix z

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

298 then show "z \<sqsubseteq> y"

299 proof

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

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

302 apply (rule Upper_antimono) apply clarify apply assumption

303 done

304 assume "z = a"

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

306 next

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

308 with y L show ?thesis by blast

309 qed

310 qed (rule Upper_closed [THEN subsetD])

311 next

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

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

314 qed

315 qed

316 qed

317 qed

319 lemma (in lattice) finite_sup_least:

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

321 proof (induct set: finite)

322 case empty

323 then show ?case by simp

324 next

325 case (insert x A)

326 show ?case

327 proof (cases "A = {}")

328 case True

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

330 next

331 case False

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

333 with _ show ?thesis

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

335 qed

336 qed

338 lemma (in lattice) finite_sup_insertI:

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

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

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

342 proof (cases "A = {}")

343 case True with P and xA show ?thesis

344 by (simp add: sup_of_singletonI)

345 next

346 case False with P and xA show ?thesis

347 by (simp add: sup_insertI finite_sup_least)

348 qed

350 lemma (in lattice) finite_sup_closed:

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

352 proof (induct set: finite)

353 case empty then show ?case by simp

354 next

355 case insert then show ?case

356 by - (rule finite_sup_insertI, simp_all)

357 qed

359 lemma (in lattice) join_left:

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

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

363 lemma (in lattice) join_right:

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

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

367 lemma (in lattice) sup_of_two_least:

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

369 proof (unfold sup_def)

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

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

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

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

374 qed

376 lemma (in lattice) join_le:

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

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

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

380 proof (rule joinI)

381 fix s

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

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

384 qed

386 lemma (in lattice) join_assoc_lemma:

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

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

389 proof (rule finite_sup_insertI)

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

391 fix s

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

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

394 proof (rule anti_sym)

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

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

397 next

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

399 by (erule_tac least_le)

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

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

402 qed (simp_all add: L)

404 lemma join_comm:

405 fixes L (structure)

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

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

409 lemma (in lattice) join_assoc:

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

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

412 proof -

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

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

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

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

417 finally show ?thesis .

418 qed

421 subsubsection {* Infimum *}

423 lemma (in lattice) meetI:

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

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

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

427 proof (unfold meet_def inf_def)

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

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

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

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

432 by (fast intro: theI2 greatest_unique P)

433 qed

435 lemma (in lattice) meet_closed [simp]:

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

437 by (rule meetI) (rule greatest_carrier)

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

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

441 by (rule greatest_LowerI) fast+

443 lemma (in partial_order) inf_of_singleton [simp]:

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

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

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

449 lemma (in lattice) inf_insertI:

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

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

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

453 proof (unfold inf_def)

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

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

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

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

458 from L inf_of_two_exists greatest_a

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

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

461 proof (rule theI2)

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

463 proof (rule greatest_LowerI)

464 fix z

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

466 then show "i \<sqsubseteq> z"

467 proof

468 assume "z = x" then show ?thesis

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

470 next

471 assume "z \<in> A"

472 with L greatest_i greatest_a show ?thesis

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

474 qed

475 next

476 fix y

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

478 show "y \<sqsubseteq> i"

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

480 fix z

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

482 then show "y \<sqsubseteq> z"

483 proof

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

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

486 apply (rule Lower_antimono) apply clarify apply assumption

487 done

488 assume "z = a"

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

490 next

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

492 with y L show ?thesis by blast

493 qed

494 qed (rule Lower_closed [THEN subsetD])

495 next

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

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

498 qed

499 next

500 fix g

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

502 show "g = i"

503 proof (rule greatest_unique)

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

505 proof (rule greatest_LowerI)

506 fix z

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

508 then show "i \<sqsubseteq> z"

509 proof

510 assume "z = x" then show ?thesis

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

512 next

513 assume "z \<in> A"

514 with L greatest_i greatest_a show ?thesis

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

516 qed

517 next

518 fix y

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

520 show "y \<sqsubseteq> i"

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

522 fix z

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

524 then show "y \<sqsubseteq> z"

525 proof

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

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

528 apply (rule Lower_antimono) apply clarify apply assumption

529 done

530 assume "z = a"

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

532 next

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

534 with y L show ?thesis by blast

535 qed

536 qed (rule Lower_closed [THEN subsetD])

537 next

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

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

540 qed

541 qed

542 qed

543 qed

545 lemma (in lattice) finite_inf_greatest:

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

547 proof (induct set: finite)

548 case empty then show ?case by simp

549 next

550 case (insert x A)

551 show ?case

552 proof (cases "A = {}")

553 case True

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

555 next

556 case False

557 from insert show ?thesis

558 proof (rule_tac inf_insertI)

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

560 qed simp_all

561 qed

562 qed

564 lemma (in lattice) finite_inf_insertI:

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

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

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

568 proof (cases "A = {}")

569 case True with P and xA show ?thesis

570 by (simp add: inf_of_singletonI)

571 next

572 case False with P and xA show ?thesis

573 by (simp add: inf_insertI finite_inf_greatest)

574 qed

576 lemma (in lattice) finite_inf_closed:

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

578 proof (induct set: finite)

579 case empty then show ?case by simp

580 next

581 case insert then show ?case

582 by (rule_tac finite_inf_insertI) (simp_all)

583 qed

585 lemma (in lattice) meet_left:

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

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

589 lemma (in lattice) meet_right:

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

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

593 lemma (in lattice) inf_of_two_greatest:

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

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

596 proof (unfold inf_def)

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

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

599 with L

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

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

602 qed

604 lemma (in lattice) meet_le:

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

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

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

608 proof (rule meetI)

609 fix i

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

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

612 qed

614 lemma (in lattice) meet_assoc_lemma:

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

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

617 proof (rule finite_inf_insertI)

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

619 fix i

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

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

622 proof (rule anti_sym)

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

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

625 next

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

627 by (erule_tac greatest_le)

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

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

630 qed (simp_all add: L)

632 lemma meet_comm:

633 fixes L (structure)

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

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

637 lemma (in lattice) meet_assoc:

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

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

640 proof -

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

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

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

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

645 finally show ?thesis .

646 qed

649 subsection {* Total Orders *}

651 locale total_order = lattice +

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

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

656 lemma (in partial_order) total_orderI:

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

658 shows "total_order L"

659 proof intro_locales

660 show "lattice_axioms L"

661 proof (rule lattice_axioms.intro)

662 fix x y

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

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

665 proof -

666 note total L

667 moreover

668 {

669 assume "x \<sqsubseteq> y"

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

671 by (rule_tac least_UpperI) auto

672 }

673 moreover

674 {

675 assume "y \<sqsubseteq> x"

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

677 by (rule_tac least_UpperI) auto

678 }

679 ultimately show ?thesis by blast

680 qed

681 next

682 fix x y

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

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

685 proof -

686 note total L

687 moreover

688 {

689 assume "y \<sqsubseteq> x"

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

691 by (rule_tac greatest_LowerI) auto

692 }

693 moreover

694 {

695 assume "x \<sqsubseteq> y"

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

697 by (rule_tac greatest_LowerI) auto

698 }

699 ultimately show ?thesis by blast

700 qed

701 qed

702 qed (assumption | rule total_order_axioms.intro)+

705 subsection {* Complete lattices *}

707 locale complete_lattice = lattice +

708 assumes sup_exists:

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

710 and inf_exists:

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

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

715 lemma (in partial_order) complete_latticeI:

716 assumes sup_exists:

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

718 and inf_exists:

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

720 shows "complete_lattice L"

721 proof intro_locales

722 show "lattice_axioms L"

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

724 qed (assumption | rule complete_lattice_axioms.intro)+

726 constdefs (structure L)

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

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

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

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

734 lemma (in complete_lattice) supI:

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

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

737 proof (unfold sup_def)

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

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

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

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

742 by (fast intro: theI2 least_unique P)

743 qed

745 lemma (in complete_lattice) sup_closed [simp]:

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

747 by (rule supI) simp_all

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

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

751 by (unfold top_def) simp

753 lemma (in complete_lattice) infI:

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

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

756 proof (unfold inf_def)

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

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

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

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

761 by (fast intro: theI2 greatest_unique P)

762 qed

764 lemma (in complete_lattice) inf_closed [simp]:

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

766 by (rule infI) simp_all

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

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

770 by (unfold bottom_def) simp

772 text {* Jacobson: Theorem 8.1 *}

774 lemma Lower_empty [simp]:

775 "Lower L {} = carrier L"

776 by (unfold Lower_def) simp

778 lemma Upper_empty [simp]:

779 "Upper L {} = carrier L"

780 by (unfold Upper_def) simp

782 theorem (in partial_order) complete_lattice_criterion1:

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

784 and inf_exists:

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

786 shows "complete_lattice L"

787 proof (rule complete_latticeI)

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

789 fix A

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

791 let ?B = "Upper L A"

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

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

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

795 from inf_exists [OF B_L B_non_empty]

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

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

798 apply (rule least_UpperI)

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

800 apply (rule b_inf_B)

801 apply (rule Lower_memI)

802 apply (erule UpperD)

803 apply assumption

804 apply (rule L)

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

806 apply (erule greatest_Lower_above [OF b_inf_B])

807 apply simp

808 apply (rule L)

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

810 done

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

812 next

813 fix A

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

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

816 proof (cases "A = {}")

817 case True then show ?thesis

818 by (simp add: top_exists)

819 next

820 case False with L show ?thesis

821 by (rule inf_exists)

822 qed

823 qed

825 (* TODO: prove dual version *)

828 subsection {* Examples *}

830 subsubsection {* Powerset of a Set is a Complete Lattice *}

832 theorem powerset_is_complete_lattice:

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

834 (is "complete_lattice ?L")

835 proof (rule partial_order.complete_latticeI)

836 show "partial_order ?L"

837 by (rule partial_order.intro) auto

838 next

839 fix B

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

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

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

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

844 next

845 fix B

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

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

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

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

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

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

852 qed

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

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

857 end