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

src/HOL/Algebra/Lattice.thy

author | wenzelm |

Thu May 06 14:14:18 2004 +0200 (2004-05-06) | |

changeset 14706 | 71590b7733b7 |

parent 14693 | 4deda204e1d8 |

child 14751 | 0d7850e27fed |

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

tuned document;

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 = Group:

12 subsection {* Partial Orders *}

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

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

17 locale partial_order = struct L +

18 assumes refl [intro, simp]:

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

20 and anti_sym [intro]:

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

22 and trans [trans]:

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

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

26 constdefs (structure L)

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

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

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

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

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

33 carrier L"

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

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

37 carrier L"

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

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

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

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

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

46 -- {* Supremum and infimum *}

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

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

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

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

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

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

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

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

60 subsubsection {* Upper *}

62 lemma Upper_closed [intro, simp]:

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

64 by (unfold Upper_def) clarify

66 lemma UpperD [dest]:

67 includes struct L

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

69 by (unfold Upper_def) blast

71 lemma Upper_memI:

72 includes struct L

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

74 by (unfold Upper_def) blast

76 lemma Upper_antimono:

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

78 by (unfold Upper_def) blast

81 subsubsection {* Lower *}

83 lemma Lower_closed [intro, simp]:

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

85 by (unfold Lower_def) clarify

87 lemma LowerD [dest]:

88 includes struct L

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

90 by (unfold Lower_def) blast

92 lemma Lower_memI:

93 includes struct L

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

95 by (unfold Lower_def) blast

97 lemma Lower_antimono:

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

99 by (unfold Lower_def) blast

102 subsubsection {* least *}

104 lemma least_carrier [intro, simp]:

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

106 by (unfold least_def) fast

108 lemma least_mem:

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

110 by (unfold least_def) fast

112 lemma (in partial_order) least_unique:

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

114 by (unfold least_def) blast

116 lemma least_le:

117 includes struct L

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

119 by (unfold least_def) fast

121 lemma least_UpperI:

122 includes struct L

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

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

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

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

127 proof -

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

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

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

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

132 qed

135 subsubsection {* greatest *}

137 lemma greatest_carrier [intro, simp]:

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

139 by (unfold greatest_def) fast

141 lemma greatest_mem:

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

143 by (unfold greatest_def) fast

145 lemma (in partial_order) greatest_unique:

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

147 by (unfold greatest_def) blast

149 lemma greatest_le:

150 includes struct L

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

152 by (unfold greatest_def) fast

154 lemma greatest_LowerI:

155 includes struct L

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

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

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

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

160 proof -

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

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

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

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

165 qed

168 subsection {* Lattices *}

170 locale lattice = partial_order +

171 assumes sup_of_two_exists:

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

173 and inf_of_two_exists:

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

176 lemma least_Upper_above:

177 includes struct L

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

179 by (unfold least_def) blast

181 lemma greatest_Lower_above:

182 includes struct L

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

184 by (unfold greatest_def) blast

187 subsubsection {* Supremum *}

189 lemma (in lattice) joinI:

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

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

192 proof (unfold join_def sup_def)

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

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

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

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

197 by (fast intro: theI2 least_unique P)

198 qed

200 lemma (in lattice) join_closed [simp]:

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

202 by (rule joinI) (rule least_carrier)

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

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

206 by (rule least_UpperI) fast+

208 lemma (in partial_order) sup_of_singleton [simp]:

209 includes struct L

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

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

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

216 lemma (in lattice) sup_insertI:

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

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

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

220 proof (unfold sup_def)

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

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

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

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

225 from L sup_of_two_exists least_a

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

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

228 proof (rule theI2)

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

230 proof (rule least_UpperI)

231 fix z

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

233 then show "z \<sqsubseteq> s"

234 proof

235 assume "z = x" then show ?thesis

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

237 next

238 assume "z \<in> A"

239 with L least_s least_a show ?thesis

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

241 qed

242 next

243 fix y

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

245 show "s \<sqsubseteq> y"

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

247 fix z

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

249 then show "z \<sqsubseteq> y"

250 proof

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

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

253 apply (rule Upper_antimono) apply clarify apply assumption

254 done

255 assume "z = a"

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

257 next

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

259 with y L show ?thesis by blast

260 qed

261 qed (rule Upper_closed [THEN subsetD])

262 next

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

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

265 qed

266 next

267 fix l

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

269 show "l = s"

270 proof (rule least_unique)

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

272 proof (rule least_UpperI)

273 fix z

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

275 then show "z \<sqsubseteq> s"

276 proof

277 assume "z = x" then show ?thesis

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

279 next

280 assume "z \<in> A"

281 with L least_s least_a show ?thesis

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

283 qed

284 next

285 fix y

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

287 show "s \<sqsubseteq> y"

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

289 fix z

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

291 then show "z \<sqsubseteq> y"

292 proof

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

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

295 apply (rule Upper_antimono) apply clarify apply assumption

296 done

297 assume "z = a"

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

299 next

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

301 with y L show ?thesis by blast

302 qed

303 qed (rule Upper_closed [THEN subsetD])

304 next

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

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

307 qed

308 qed

309 qed

310 qed

312 lemma (in lattice) finite_sup_least:

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

314 proof (induct set: Finites)

315 case empty

316 then show ?case by simp

317 next

318 case (insert A x)

319 show ?case

320 proof (cases "A = {}")

321 case True

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

323 next

324 case False

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

326 with _ show ?thesis

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

328 qed

329 qed

331 lemma (in lattice) finite_sup_insertI:

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

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

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

335 proof (cases "A = {}")

336 case True with P and xA show ?thesis

337 by (simp add: sup_of_singletonI)

338 next

339 case False with P and xA show ?thesis

340 by (simp add: sup_insertI finite_sup_least)

341 qed

343 lemma (in lattice) finite_sup_closed:

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

345 proof (induct set: Finites)

346 case empty then show ?case by simp

347 next

348 case (insert A x) then show ?case

349 by - (rule finite_sup_insertI, simp_all)

350 qed

352 lemma (in lattice) join_left:

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

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

356 lemma (in lattice) join_right:

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

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

360 lemma (in lattice) sup_of_two_least:

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

362 proof (unfold sup_def)

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

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

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

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

367 qed

369 lemma (in lattice) join_le:

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

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

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

373 proof (rule joinI)

374 fix s

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

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

377 qed

379 lemma (in lattice) join_assoc_lemma:

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

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

382 proof (rule finite_sup_insertI)

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

384 fix s

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

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

387 proof (rule anti_sym)

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

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

390 next

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

392 by (erule_tac least_le)

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

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

395 qed (simp_all add: L)

397 lemma join_comm:

398 includes struct L

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

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

402 lemma (in lattice) join_assoc:

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

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

405 proof -

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

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

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

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

410 finally show ?thesis .

411 qed

414 subsubsection {* Infimum *}

416 lemma (in lattice) meetI:

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

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

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

420 proof (unfold meet_def inf_def)

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

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

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

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

425 by (fast intro: theI2 greatest_unique P)

426 qed

428 lemma (in lattice) meet_closed [simp]:

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

430 by (rule meetI) (rule greatest_carrier)

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

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

434 by (rule greatest_LowerI) fast+

436 lemma (in partial_order) inf_of_singleton [simp]:

437 includes struct L

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

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

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

443 lemma (in lattice) inf_insertI:

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

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

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

447 proof (unfold inf_def)

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

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

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

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

452 from L inf_of_two_exists greatest_a

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

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

455 proof (rule theI2)

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

457 proof (rule greatest_LowerI)

458 fix z

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

460 then show "i \<sqsubseteq> z"

461 proof

462 assume "z = x" then show ?thesis

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

464 next

465 assume "z \<in> A"

466 with L greatest_i greatest_a show ?thesis

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

468 qed

469 next

470 fix y

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

472 show "y \<sqsubseteq> i"

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

474 fix z

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

476 then show "y \<sqsubseteq> z"

477 proof

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

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

480 apply (rule Lower_antimono) apply clarify apply assumption

481 done

482 assume "z = a"

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

484 next

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

486 with y L show ?thesis by blast

487 qed

488 qed (rule Lower_closed [THEN subsetD])

489 next

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

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

492 qed

493 next

494 fix g

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

496 show "g = i"

497 proof (rule greatest_unique)

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

499 proof (rule greatest_LowerI)

500 fix z

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

502 then show "i \<sqsubseteq> z"

503 proof

504 assume "z = x" then show ?thesis

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

506 next

507 assume "z \<in> A"

508 with L greatest_i greatest_a show ?thesis

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

510 qed

511 next

512 fix y

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

514 show "y \<sqsubseteq> i"

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

516 fix z

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

518 then show "y \<sqsubseteq> z"

519 proof

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

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

522 apply (rule Lower_antimono) apply clarify apply assumption

523 done

524 assume "z = a"

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

526 next

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

528 with y L show ?thesis by blast

529 qed

530 qed (rule Lower_closed [THEN subsetD])

531 next

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

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

534 qed

535 qed

536 qed

537 qed

539 lemma (in lattice) finite_inf_greatest:

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

541 proof (induct set: Finites)

542 case empty then show ?case by simp

543 next

544 case (insert A x)

545 show ?case

546 proof (cases "A = {}")

547 case True

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

549 next

550 case False

551 from insert show ?thesis

552 proof (rule_tac inf_insertI)

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

554 qed simp_all

555 qed

556 qed

558 lemma (in lattice) finite_inf_insertI:

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

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

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

562 proof (cases "A = {}")

563 case True with P and xA show ?thesis

564 by (simp add: inf_of_singletonI)

565 next

566 case False with P and xA show ?thesis

567 by (simp add: inf_insertI finite_inf_greatest)

568 qed

570 lemma (in lattice) finite_inf_closed:

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

572 proof (induct set: Finites)

573 case empty then show ?case by simp

574 next

575 case (insert A x) then show ?case

576 by (rule_tac finite_inf_insertI) (simp_all)

577 qed

579 lemma (in lattice) meet_left:

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

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

583 lemma (in lattice) meet_right:

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

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

587 lemma (in lattice) inf_of_two_greatest:

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

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

590 proof (unfold inf_def)

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

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

593 with L

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

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

596 qed

598 lemma (in lattice) meet_le:

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

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

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

602 proof (rule meetI)

603 fix i

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

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

606 qed

608 lemma (in lattice) meet_assoc_lemma:

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

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

611 proof (rule finite_inf_insertI)

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

613 fix i

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

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

616 proof (rule anti_sym)

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

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

619 next

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

621 by (erule_tac greatest_le)

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

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

624 qed (simp_all add: L)

626 lemma meet_comm:

627 includes struct L

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

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

631 lemma (in lattice) meet_assoc:

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

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

634 proof -

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

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

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

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

639 finally show ?thesis .

640 qed

643 subsection {* Total Orders *}

645 locale total_order = lattice +

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

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

650 lemma (in partial_order) total_orderI:

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

652 shows "total_order L"

653 proof (rule total_order.intro)

654 show "lattice_axioms L"

655 proof (rule lattice_axioms.intro)

656 fix x y

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

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

659 proof -

660 note total L

661 moreover

662 {

663 assume "x \<sqsubseteq> y"

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

665 by (rule_tac least_UpperI) auto

666 }

667 moreover

668 {

669 assume "y \<sqsubseteq> x"

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

671 by (rule_tac least_UpperI) auto

672 }

673 ultimately show ?thesis by blast

674 qed

675 next

676 fix x y

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

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

679 proof -

680 note total L

681 moreover

682 {

683 assume "y \<sqsubseteq> x"

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

685 by (rule_tac greatest_LowerI) auto

686 }

687 moreover

688 {

689 assume "x \<sqsubseteq> y"

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

691 by (rule_tac greatest_LowerI) auto

692 }

693 ultimately show ?thesis by blast

694 qed

695 qed

696 qed (assumption | rule total_order_axioms.intro)+

699 subsection {* Complete lattices *}

701 locale complete_lattice = lattice +

702 assumes sup_exists:

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

704 and inf_exists:

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

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

709 lemma (in partial_order) complete_latticeI:

710 assumes sup_exists:

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

712 and inf_exists:

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

714 shows "complete_lattice L"

715 proof (rule complete_lattice.intro)

716 show "lattice_axioms L"

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

718 qed (assumption | rule complete_lattice_axioms.intro)+

720 constdefs (structure L)

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

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

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

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

728 lemma (in complete_lattice) supI:

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

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

731 proof (unfold sup_def)

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

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

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

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

736 by (fast intro: theI2 least_unique P)

737 qed

739 lemma (in complete_lattice) sup_closed [simp]:

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

741 by (rule supI) simp_all

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

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

745 by (unfold top_def) simp

747 lemma (in complete_lattice) infI:

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

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

750 proof (unfold inf_def)

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

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

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

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

755 by (fast intro: theI2 greatest_unique P)

756 qed

758 lemma (in complete_lattice) inf_closed [simp]:

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

760 by (rule infI) simp_all

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

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

764 by (unfold bottom_def) simp

766 text {* Jacobson: Theorem 8.1 *}

768 lemma Lower_empty [simp]:

769 "Lower L {} = carrier L"

770 by (unfold Lower_def) simp

772 lemma Upper_empty [simp]:

773 "Upper L {} = carrier L"

774 by (unfold Upper_def) simp

776 theorem (in partial_order) complete_lattice_criterion1:

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

778 and inf_exists:

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

780 shows "complete_lattice L"

781 proof (rule complete_latticeI)

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

783 fix A

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

785 let ?B = "Upper L A"

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

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

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

789 from inf_exists [OF B_L B_non_empty]

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

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

792 apply (rule least_UpperI)

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

794 apply (rule b_inf_B)

795 apply (rule Lower_memI)

796 apply (erule UpperD)

797 apply assumption

798 apply (rule L)

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

800 apply (erule greatest_Lower_above [OF b_inf_B])

801 apply simp

802 apply (rule L)

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

804 done

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

806 next

807 fix A

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

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

810 proof (cases "A = {}")

811 case True then show ?thesis

812 by (simp add: top_exists)

813 next

814 case False with L show ?thesis

815 by (rule inf_exists)

816 qed

817 qed

819 (* TODO: prove dual version *)

821 subsection {* Examples *}

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

825 theorem powerset_is_complete_lattice:

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

827 (is "complete_lattice ?L")

828 proof (rule partial_order.complete_latticeI)

829 show "partial_order ?L"

830 by (rule partial_order.intro) auto

831 next

832 fix B

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

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

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

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

837 next

838 fix B

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

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

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

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

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

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

845 qed

847 subsubsection {* Lattice of subgroups of a group *}

849 theorem (in group) subgroups_partial_order:

850 "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"

851 by (rule partial_order.intro) simp_all

853 lemma (in group) subgroup_self:

854 "subgroup (carrier G) G"

855 by (rule subgroupI) auto

857 lemma (in group) subgroup_imp_group:

858 "subgroup H G ==> group (G(| carrier := H |))"

859 using subgroup.groupI [OF _ group.intro] .

861 lemma (in group) is_monoid [intro, simp]:

862 "monoid G"

863 by (rule monoid.intro)

865 lemma (in group) subgroup_inv_equality:

866 "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"

867 apply (rule_tac inv_equality [THEN sym])

868 apply (rule group.l_inv [OF subgroup_imp_group, simplified])

869 apply assumption+

870 apply (rule subsetD [OF subgroup.subset])

871 apply assumption+

872 apply (rule subsetD [OF subgroup.subset])

873 apply assumption

874 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified])

875 apply assumption+

876 done

878 theorem (in group) subgroups_Inter:

879 assumes subgr: "(!!H. H \<in> A ==> subgroup H G)"

880 and not_empty: "A ~= {}"

881 shows "subgroup (\<Inter>A) G"

882 proof (rule subgroupI)

883 from subgr [THEN subgroup.subset] and not_empty

884 show "\<Inter>A \<subseteq> carrier G" by blast

885 next

886 from subgr [THEN subgroup.one_closed]

887 show "\<Inter>A ~= {}" by blast

888 next

889 fix x assume "x \<in> \<Inter>A"

890 with subgr [THEN subgroup.m_inv_closed]

891 show "inv x \<in> \<Inter>A" by blast

892 next

893 fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A"

894 with subgr [THEN subgroup.m_closed]

895 show "x \<otimes> y \<in> \<Inter>A" by blast

896 qed

898 theorem (in group) subgroups_complete_lattice:

899 "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"

900 (is "complete_lattice ?L")

901 proof (rule partial_order.complete_lattice_criterion1)

902 show "partial_order ?L" by (rule subgroups_partial_order)

903 next

904 have "greatest ?L (carrier G) (carrier ?L)"

905 by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)

906 then show "EX G. greatest ?L G (carrier ?L)" ..

907 next

908 fix A

909 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"

910 then have Int_subgroup: "subgroup (\<Inter>A) G"

911 by (fastsimp intro: subgroups_Inter)

912 have "greatest ?L (\<Inter>A) (Lower ?L A)"

913 (is "greatest ?L ?Int _")

914 proof (rule greatest_LowerI)

915 fix H

916 assume H: "H \<in> A"

917 with L have subgroupH: "subgroup H G" by auto

918 from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms)

919 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")

920 by (rule subgroup_imp_group)

921 from groupH have monoidH: "monoid ?H"

922 by (rule group.is_monoid)

923 from H have Int_subset: "?Int \<subseteq> H" by fastsimp

924 then show "le ?L ?Int H" by simp

925 next

926 fix H

927 assume H: "H \<in> Lower ?L A"

928 with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest)

929 next

930 show "A \<subseteq> carrier ?L" by (rule L)

931 next

932 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)

933 qed

934 then show "EX I. greatest ?L I (Lower ?L A)" ..

935 qed

937 end