author  haftmann 
Sat, 18 Mar 2006 09:58:49 +0100  
changeset 19286  83404ccd270a 
parent 16417  9bc16273c2d4 
child 19783  82f365a14960 
permissions  rwrr 
14551  1 
(* 
14706  2 
Title: HOL/Algebra/Lattice.thy 
14551  3 
Id: $Id$ 
4 
Author: Clemens Ballarin, started 7 November 2003 

5 
Copyright: Clemens Ballarin 

6 
*) 

7 

14706  8 
header {* Orders and Lattices *} 
14551  9 

16417  10 
theory Lattice imports Main begin 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

11 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

12 
text {* Object with a carrier set. *} 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

13 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

14 
record 'a partial_object = 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

15 
carrier :: "'a set" 
14551  16 

17 
subsection {* Partial Orders *} 

18 

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

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

21 

14693  22 
locale partial_order = struct L + 
14551  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" 

30 

14651  31 
constdefs (structure L) 
19286  32 
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) 
14651  33 
"x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" 
14551  34 

14651  35 
 {* Upper and lower bounds of a set. *} 
36 
Upper :: "[_, 'a set] => 'a set" 

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

14651  40 
Lower :: "[_, 'a set] => 'a set" 
14693  41 
"Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L > l \<sqsubseteq> x)} \<inter> 
14551  42 
carrier L" 
43 

14651  44 
 {* Least and greatest, as predicate. *} 
45 
least :: "[_, 'a, 'a set] => bool" 

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

14651  48 
greatest :: "[_, 'a, 'a set] => bool" 
14693  49 
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" 
14551  50 

14651  51 
 {* Supremum and infimum *} 
52 
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) 

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

14551  54 

14651  55 
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) 
56 
"\<Sqinter>A == THE x. greatest L x (Lower L A)" 

14551  57 

14651  58 
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) 
59 
"x \<squnion> y == sup L {x, y}" 

14551  60 

16325
a6431098a929
Fixed "axiom" generation for mixed locales with and without predicates.
ballarin
parents:
15328
diff
changeset

61 
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) 
14651  62 
"x \<sqinter> y == inf L {x, y}" 
14551  63 

14651  64 

65 
subsubsection {* Upper *} 

14551  66 

67 
lemma Upper_closed [intro, simp]: 

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

69 
by (unfold Upper_def) clarify 

70 

71 
lemma UpperD [dest]: 

14693  72 
includes struct L 
14551  73 
shows "[ u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> u" 
14693  74 
by (unfold Upper_def) blast 
14551  75 

76 
lemma Upper_memI: 

14693  77 
includes struct L 
14551  78 
shows "[ !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L ] ==> x \<in> Upper L A" 
14693  79 
by (unfold Upper_def) blast 
14551  80 

81 
lemma Upper_antimono: 

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

83 
by (unfold Upper_def) blast 

84 

14651  85 

86 
subsubsection {* Lower *} 

14551  87 

88 
lemma Lower_closed [intro, simp]: 

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

90 
by (unfold Lower_def) clarify 

91 

92 
lemma LowerD [dest]: 

14693  93 
includes struct L 
14551  94 
shows "[ l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L ] ==> l \<sqsubseteq> x" 
14693  95 
by (unfold Lower_def) blast 
14551  96 

97 
lemma Lower_memI: 

14693  98 
includes struct L 
14551  99 
shows "[ !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L ] ==> x \<in> Lower L A" 
14693  100 
by (unfold Lower_def) blast 
14551  101 

102 
lemma Lower_antimono: 

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

104 
by (unfold Lower_def) blast 

105 

14651  106 

107 
subsubsection {* least *} 

14551  108 

109 
lemma least_carrier [intro, simp]: 

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

111 
by (unfold least_def) fast 

112 

113 
lemma least_mem: 

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

115 
by (unfold least_def) fast 

116 

117 
lemma (in partial_order) least_unique: 

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

119 
by (unfold least_def) blast 

120 

121 
lemma least_le: 

14693  122 
includes struct L 
14551  123 
shows "[ least L x A; a \<in> A ] ==> x \<sqsubseteq> a" 
124 
by (unfold least_def) fast 

125 

126 
lemma least_UpperI: 

14693  127 
includes struct L 
14551  128 
assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" 
129 
and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" 

14693  130 
and L: "A \<subseteq> carrier L" "s \<in> carrier L" 
14551  131 
shows "least L s (Upper L A)" 
14693  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) 

14551  137 
qed 
138 

14651  139 

140 
subsubsection {* greatest *} 

14551  141 

142 
lemma greatest_carrier [intro, simp]: 

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

144 
by (unfold greatest_def) fast 

145 

146 
lemma greatest_mem: 

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

148 
by (unfold greatest_def) fast 

149 

150 
lemma (in partial_order) greatest_unique: 

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

152 
by (unfold greatest_def) blast 

153 

154 
lemma greatest_le: 

14693  155 
includes struct L 
14551  156 
shows "[ greatest L x A; a \<in> A ] ==> a \<sqsubseteq> x" 
157 
by (unfold greatest_def) fast 

158 

159 
lemma greatest_LowerI: 

14693  160 
includes struct L 
14551  161 
assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" 
162 
and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" 

14693  163 
and L: "A \<subseteq> carrier L" "i \<in> carrier L" 
14551  164 
shows "greatest L i (Lower L A)" 
14693  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) 

14551  170 
qed 
171 

14693  172 

14551  173 
subsection {* Lattices *} 
174 

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})" 

180 

181 
lemma least_Upper_above: 

14693  182 
includes struct L 
14551  183 
shows "[ least L s (Upper L A); x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> s" 
184 
by (unfold least_def) blast 

185 

186 
lemma greatest_Lower_above: 

14693  187 
includes struct L 
14551  188 
shows "[ greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L ] ==> i \<sqsubseteq> x" 
189 
by (unfold greatest_def) blast 

190 

14666  191 

14551  192 
subsubsection {* Supremum *} 
193 

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) 

14693  198 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
14551  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}))" 

14693  202 
by (fast intro: theI2 least_unique P) 
14551  203 
qed 
204 

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) 

208 

14651  209 
lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) 
14551  210 
"x \<in> carrier L ==> least L x (Upper L {x})" 
211 
by (rule least_UpperI) fast+ 

212 

213 
lemma (in partial_order) sup_of_singleton [simp]: 

14693  214 
includes struct L 
215 
shows "x \<in> carrier L ==> \<Squnion>{x} = x" 

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

14666  218 

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

14551  220 

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 ] 

14693  224 
==> P (\<Squnion>(insert x A))" 
14551  225 
proof (unfold sup_def) 
14693  226 
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  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)))" 

14693  233 
proof (rule theI2) 
14551  234 
show "least L s (Upper L (insert x A))" 
235 
proof (rule least_UpperI) 

236 
fix z 

14693  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 

14551  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) 

14693  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) 

14551  288 
qed 
289 
next 

14693  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]) 

14551  309 
next 
14693  310 
from L show "insert x A \<subseteq> carrier L" by simp 
311 
from least_s show "s \<in> carrier L" by simp 

14551  312 
qed 
313 
qed 

314 
qed 

315 
qed 

316 

317 
lemma (in lattice) finite_sup_least: 

14693  318 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> least L (\<Squnion>A) (Upper L A)" 
14551  319 
proof (induct set: Finites) 
14693  320 
case empty 
321 
then show ?case by simp 

14551  322 
next 
15328  323 
case (insert x A) 
14551  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 

14693  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]) 

14551  333 
qed 
334 
qed 

335 

336 
lemma (in lattice) finite_sup_insertI: 

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

14693  338 
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  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 

347 

348 
lemma (in lattice) finite_sup_closed: 

14693  349 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> \<Squnion>A \<in> carrier L" 
14551  350 
proof (induct set: Finites) 
351 
case empty then show ?case by simp 

352 
next 

15328  353 
case insert then show ?case 
14693  354 
by  (rule finite_sup_insertI, simp_all) 
14551  355 
qed 
356 

357 
lemma (in lattice) join_left: 

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

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

361 
lemma (in lattice) join_right: 

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

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

365 
lemma (in lattice) sup_of_two_least: 

14693  366 
"[ x \<in> carrier L; y \<in> carrier L ] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" 
14551  367 
proof (unfold sup_def) 
14693  368 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
14551  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 

373 

374 
lemma (in lattice) join_le: 

14693  375 
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" 
376 
and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 

14551  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 

14693  383 

14551  384 
lemma (in lattice) join_assoc_lemma: 
14693  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}" 

14551  387 
proof (rule finite_sup_insertI) 
14651  388 
 {* The textbook argument in Jacobson I, p 457 *} 
14551  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) 

401 

402 
lemma join_comm: 

14693  403 
includes struct L 
14551  404 
shows "x \<squnion> y = y \<squnion> x" 
405 
by (unfold join_def) (simp add: insert_commute) 

406 

407 
lemma (in lattice) join_assoc: 

14693  408 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
14551  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) 

14693  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) 

14551  414 
also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) 
415 
finally show ?thesis . 

416 
qed 

417 

14693  418 

14551  419 
subsubsection {* Infimum *} 
420 

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) 

14693  426 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
14551  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 

432 

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) 

436 

14651  437 
lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) 
14551  438 
"x \<in> carrier L ==> greatest L x (Lower L {x})" 
439 
by (rule greatest_LowerI) fast+ 

440 

441 
lemma (in partial_order) inf_of_singleton [simp]: 

14693  442 
includes struct L 
14551  443 
shows "x \<in> carrier L ==> \<Sqinter> {x} = x" 
444 
by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) 

445 

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

447 

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 ] 

14693  451 
==> P (\<Sqinter>(insert x A))" 
14551  452 
proof (unfold inf_def) 
14693  453 
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  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)))" 

14693  460 
proof (rule theI2) 
14551  461 
show "greatest L i (Lower L (insert x A))" 
462 
proof (rule greatest_LowerI) 

463 
fix z 

14693  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 

14551  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) 

14693  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 

14551  516 
next 
14693  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 

14551  534 
qed 
14693  535 
qed (rule Lower_closed [THEN subsetD]) 
14551  536 
next 
14693  537 
from L show "insert x A \<subseteq> carrier L" by simp 
538 
from greatest_i show "i \<in> carrier L" by simp 

14551  539 
qed 
540 
qed 

541 
qed 

542 
qed 

543 

544 
lemma (in lattice) finite_inf_greatest: 

14693  545 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> greatest L (\<Sqinter>A) (Lower L A)" 
14551  546 
proof (induct set: Finites) 
547 
case empty then show ?case by simp 

548 
next 

15328  549 
case (insert x A) 
14551  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) 

14693  558 
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp 
14551  559 
qed simp_all 
560 
qed 

561 
qed 

562 

563 
lemma (in lattice) finite_inf_insertI: 

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

14693  565 
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  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 

574 

575 
lemma (in lattice) finite_inf_closed: 

14693  576 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> \<Sqinter>A \<in> carrier L" 
14551  577 
proof (induct set: Finites) 
578 
case empty then show ?case by simp 

579 
next 

15328  580 
case insert then show ?case 
14551  581 
by (rule_tac finite_inf_insertI) (simp_all) 
582 
qed 

583 

584 
lemma (in lattice) meet_left: 

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

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

588 
lemma (in lattice) meet_right: 

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

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

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) 

14693  596 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
14551  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 

602 

603 
lemma (in lattice) meet_le: 

14693  604 
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" 
605 
and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 

14551  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 

14693  612 

14551  613 
lemma (in lattice) meet_assoc_lemma: 
14693  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}" 

14551  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) 

630 

631 
lemma meet_comm: 

14693  632 
includes struct L 
14551  633 
shows "x \<sqinter> y = y \<sqinter> x" 
634 
by (unfold meet_def) (simp add: insert_commute) 

635 

636 
lemma (in lattice) meet_assoc: 

14693  637 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
14551  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 

646 

14693  647 

14551  648 
subsection {* Total Orders *} 
649 

650 
locale total_order = lattice + 

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

652 

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

654 

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 

14693  662 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
14551  663 
show "EX s. least L s (Upper L {x, y})" 
664 
proof  

665 
note total L 

666 
moreover 

667 
{ 

14693  668 
assume "x \<sqsubseteq> y" 
14551  669 
with L have "least L y (Upper L {x, y})" 
14693  670 
by (rule_tac least_UpperI) auto 
14551  671 
} 
672 
moreover 

673 
{ 

14693  674 
assume "y \<sqsubseteq> x" 
14551  675 
with L have "least L x (Upper L {x, y})" 
14693  676 
by (rule_tac least_UpperI) auto 
14551  677 
} 
678 
ultimately show ?thesis by blast 

679 
qed 

680 
next 

681 
fix x y 

14693  682 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
14551  683 
show "EX i. greatest L i (Lower L {x, y})" 
684 
proof  

685 
note total L 

686 
moreover 

687 
{ 

14693  688 
assume "y \<sqsubseteq> x" 
14551  689 
with L have "greatest L y (Lower L {x, y})" 
14693  690 
by (rule_tac greatest_LowerI) auto 
14551  691 
} 
692 
moreover 

693 
{ 

14693  694 
assume "x \<sqsubseteq> y" 
14551  695 
with L have "greatest L x (Lower L {x, y})" 
14693  696 
by (rule_tac greatest_LowerI) auto 
14551  697 
} 
698 
ultimately show ?thesis by blast 

699 
qed 

700 
qed 

701 
qed (assumption  rule total_order_axioms.intro)+ 

702 

14693  703 

14551  704 
subsection {* Complete lattices *} 
705 

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)" 

711 

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

713 

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" 

14693  722 
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ 
14551  723 
qed (assumption  rule complete_lattice_axioms.intro)+ 
724 

14651  725 
constdefs (structure L) 
726 
top :: "_ => 'a" ("\<top>\<index>") 

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

14551  728 

14651  729 
bottom :: "_ => 'a" ("\<bottom>\<index>") 
730 
"\<bottom> == inf L (carrier L)" 

14551  731 

732 

733 
lemma (in complete_lattice) supI: 

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

14651  735 
==> P (\<Squnion>A)" 
14551  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 

743 

744 
lemma (in complete_lattice) sup_closed [simp]: 

14693  745 
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" 
14551  746 
by (rule supI) simp_all 
747 

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

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

750 
by (unfold top_def) simp 

751 

752 
lemma (in complete_lattice) infI: 

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

14693  754 
==> P (\<Sqinter>A)" 
14551  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 

762 

763 
lemma (in complete_lattice) inf_closed [simp]: 

14693  764 
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" 
14551  765 
by (rule infI) simp_all 
766 

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

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

769 
by (unfold bottom_def) simp 

770 

771 
text {* Jacobson: Theorem 8.1 *} 

772 

773 
lemma Lower_empty [simp]: 

774 
"Lower L {} = carrier L" 

775 
by (unfold Lower_def) simp 

776 

777 
lemma Upper_empty [simp]: 

778 
"Upper L {} = carrier L" 

779 
by (unfold Upper_def) simp 

780 

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) 

14693  798 
apply (rule greatest_le [where A = "Lower L ?B"]) 
14551  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 

823 

824 
(* TODO: prove dual version *) 

825 

826 
subsection {* Examples *} 

827 

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

829 

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 

851 

14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

852 
text {* An other example, that of the lattice of subgroups of a group, 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

853 
can be found in Group theory (Section~\ref{sec:subgrouplattice}). *} 
14551  854 

14693  855 
end 