14551

1 
(*


2 
Title: Orders and Lattices


3 
Id: $Id$


4 
Author: Clemens Ballarin, started 7 November 2003


5 
Copyright: Clemens Ballarin


6 
*)


7 

14577

8 
header {* Order and Lattices *}

14551

9 

14577

10 
theory Lattice = Group:

14551

11 


12 
subsection {* Partial Orders *}


13 


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


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


16 

14693

17 
locale partial_order = struct L +

14551

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"


25 

14651

26 
constdefs (structure L)


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


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

14551

29 

14651

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


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

14693

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

14551

33 
carrier L"


34 

14651

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

14693

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

14551

37 
carrier L"


38 

14651

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


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

14693

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

14551

42 

14651

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

14693

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

14551

45 

14651

46 
 {* Supremum and infimum *}


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


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

14551

49 

14651

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


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

14551

52 

14651

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


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

14551

55 

14651

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


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

14551

58 

14651

59 


60 
subsubsection {* Upper *}

14551

61 


62 
lemma Upper_closed [intro, simp]:


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


64 
by (unfold Upper_def) clarify


65 


66 
lemma UpperD [dest]:

14693

67 
includes struct L

14551

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

14693

69 
by (unfold Upper_def) blast

14551

70 


71 
lemma Upper_memI:

14693

72 
includes struct L

14551

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

14693

74 
by (unfold Upper_def) blast

14551

75 


76 
lemma Upper_antimono:


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


78 
by (unfold Upper_def) blast


79 

14651

80 


81 
subsubsection {* Lower *}

14551

82 


83 
lemma Lower_closed [intro, simp]:


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


85 
by (unfold Lower_def) clarify


86 


87 
lemma LowerD [dest]:

14693

88 
includes struct L

14551

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

14693

90 
by (unfold Lower_def) blast

14551

91 


92 
lemma Lower_memI:

14693

93 
includes struct L

14551

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

14693

95 
by (unfold Lower_def) blast

14551

96 


97 
lemma Lower_antimono:


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


99 
by (unfold Lower_def) blast


100 

14651

101 


102 
subsubsection {* least *}

14551

103 


104 
lemma least_carrier [intro, simp]:


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


106 
by (unfold least_def) fast


107 


108 
lemma least_mem:


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


110 
by (unfold least_def) fast


111 


112 
lemma (in partial_order) least_unique:


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


114 
by (unfold least_def) blast


115 


116 
lemma least_le:

14693

117 
includes struct L

14551

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


119 
by (unfold least_def) fast


120 


121 
lemma least_UpperI:

14693

122 
includes struct L

14551

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


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

14693

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

14551

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

14693

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)

14551

132 
qed


133 

14651

134 


135 
subsubsection {* greatest *}

14551

136 


137 
lemma greatest_carrier [intro, simp]:


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


139 
by (unfold greatest_def) fast


140 


141 
lemma greatest_mem:


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


143 
by (unfold greatest_def) fast


144 


145 
lemma (in partial_order) greatest_unique:


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


147 
by (unfold greatest_def) blast


148 


149 
lemma greatest_le:

14693

150 
includes struct L

14551

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


152 
by (unfold greatest_def) fast


153 


154 
lemma greatest_LowerI:

14693

155 
includes struct L

14551

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


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

14693

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

14551

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

14693

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)

14551

165 
qed


166 

14693

167 

14551

168 
subsection {* Lattices *}


169 


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


175 


176 
lemma least_Upper_above:

14693

177 
includes struct L

14551

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


179 
by (unfold least_def) blast


180 


181 
lemma greatest_Lower_above:

14693

182 
includes struct L

14551

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


184 
by (unfold greatest_def) blast


185 

14666

186 

14551

187 
subsubsection {* Supremum *}


188 


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)

14693

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

14551

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

14693

197 
by (fast intro: theI2 least_unique P)

14551

198 
qed


199 


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)


203 

14651

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

14551

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


206 
by (rule least_UpperI) fast+


207 


208 
lemma (in partial_order) sup_of_singleton [simp]:

14693

209 
includes struct L


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

14551

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


212 

14666

213 


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

14551

215 


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 ]

14693

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

14551

220 
proof (unfold sup_def)

14693

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

14551

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

14693

228 
proof (rule theI2)

14551

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


230 
proof (rule least_UpperI)


231 
fix z

14693

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

14551

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)

14693

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)

14551

283 
qed


284 
next

14693

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

14551

304 
next

14693

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


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

14551

307 
qed


308 
qed


309 
qed


310 
qed


311 


312 
lemma (in lattice) finite_sup_least:

14693

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

14551

314 
proof (induct set: Finites)

14693

315 
case empty


316 
then show ?case by simp

14551

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

14693

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

14551

328 
qed


329 
qed


330 


331 
lemma (in lattice) finite_sup_insertI:


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

14693

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

14551

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


342 


343 
lemma (in lattice) finite_sup_closed:

14693

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

14551

345 
proof (induct set: Finites)


346 
case empty then show ?case by simp


347 
next


348 
case (insert A x) then show ?case

14693

349 
by  (rule finite_sup_insertI, simp_all)

14551

350 
qed


351 


352 
lemma (in lattice) join_left:


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

14693

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

14551

355 


356 
lemma (in lattice) join_right:


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

14693

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

14551

359 


360 
lemma (in lattice) sup_of_two_least:

14693

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

14551

362 
proof (unfold sup_def)

14693

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

14551

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


368 


369 
lemma (in lattice) join_le:

14693

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


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

14551

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

14693

378 

14551

379 
lemma (in lattice) join_assoc_lemma:

14693

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

14551

382 
proof (rule finite_sup_insertI)

14651

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

14551

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)


396 


397 
lemma join_comm:

14693

398 
includes struct L

14551

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


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


401 


402 
lemma (in lattice) join_assoc:

14693

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

14551

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)

14693

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)

14551

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


410 
finally show ?thesis .


411 
qed


412 

14693

413 

14551

414 
subsubsection {* Infimum *}


415 


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)

14693

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

14551

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


427 


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)


431 

14651

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

14551

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


434 
by (rule greatest_LowerI) fast+


435 


436 
lemma (in partial_order) inf_of_singleton [simp]:

14693

437 
includes struct L

14551

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


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


440 


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


442 


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 ]

14693

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

14551

447 
proof (unfold inf_def)

14693

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

14551

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

14693

455 
proof (rule theI2)

14551

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


457 
proof (rule greatest_LowerI)


458 
fix z

14693

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

14551

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)

14693

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

14551

511 
next

14693

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

14551

529 
qed

14693

530 
qed (rule Lower_closed [THEN subsetD])

14551

531 
next

14693

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


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

14551

534 
qed


535 
qed


536 
qed


537 
qed


538 


539 
lemma (in lattice) finite_inf_greatest:

14693

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

14551

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)

14693

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

14551

554 
qed simp_all


555 
qed


556 
qed


557 


558 
lemma (in lattice) finite_inf_insertI:


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

14693

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

14551

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


569 


570 
lemma (in lattice) finite_inf_closed:

14693

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

14551

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


578 


579 
lemma (in lattice) meet_left:


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

14693

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

14551

582 


583 
lemma (in lattice) meet_right:


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

14693

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

14551

586 


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)

14693

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

14551

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


597 


598 
lemma (in lattice) meet_le:

14693

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


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

14551

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

14693

607 

14551

608 
lemma (in lattice) meet_assoc_lemma:

14693

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

14551

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)


625 


626 
lemma meet_comm:

14693

627 
includes struct L

14551

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


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


630 


631 
lemma (in lattice) meet_assoc:

14693

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

14551

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


641 

14693

642 

14551

643 
subsection {* Total Orders *}


644 


645 
locale total_order = lattice +


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


647 


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


649 


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

14693

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

14551

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


659 
proof 


660 
note total L


661 
moreover


662 
{

14693

663 
assume "x \<sqsubseteq> y"

14551

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

14693

665 
by (rule_tac least_UpperI) auto

14551

666 
}


667 
moreover


668 
{

14693

669 
assume "y \<sqsubseteq> x"

14551

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

14693

671 
by (rule_tac least_UpperI) auto

14551

672 
}


673 
ultimately show ?thesis by blast


674 
qed


675 
next


676 
fix x y

14693

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

14551

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


679 
proof 


680 
note total L


681 
moreover


682 
{

14693

683 
assume "y \<sqsubseteq> x"

14551

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

14693

685 
by (rule_tac greatest_LowerI) auto

14551

686 
}


687 
moreover


688 
{

14693

689 
assume "x \<sqsubseteq> y"

14551

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

14693

691 
by (rule_tac greatest_LowerI) auto

14551

692 
}


693 
ultimately show ?thesis by blast


694 
qed


695 
qed


696 
qed (assumption  rule total_order_axioms.intro)+


697 

14693

698 

14551

699 
subsection {* Complete lattices *}


700 


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


706 


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


708 


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"

14693

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

14551

718 
qed (assumption  rule complete_lattice_axioms.intro)+


719 

14651

720 
constdefs (structure L)


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


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

14551

723 

14651

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


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

14551

726 


727 


728 
lemma (in complete_lattice) supI:


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

14651

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

14551

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


738 


739 
lemma (in complete_lattice) sup_closed [simp]:

14693

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

14551

741 
by (rule supI) simp_all


742 


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


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


745 
by (unfold top_def) simp


746 


747 
lemma (in complete_lattice) infI:


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

14693

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

14551

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


757 


758 
lemma (in complete_lattice) inf_closed [simp]:

14693

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

14551

760 
by (rule infI) simp_all


761 


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


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


764 
by (unfold bottom_def) simp


765 


766 
text {* Jacobson: Theorem 8.1 *}


767 


768 
lemma Lower_empty [simp]:


769 
"Lower L {} = carrier L"


770 
by (unfold Lower_def) simp


771 


772 
lemma Upper_empty [simp]:


773 
"Upper L {} = carrier L"


774 
by (unfold Upper_def) simp


775 


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)

14693

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

14551

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


818 


819 
(* TODO: prove dual version *)


820 


821 
subsection {* Examples *}


822 


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


824 


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


846 


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


848 


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


852 


853 
lemma (in group) subgroup_self:


854 
"subgroup (carrier G) G"


855 
by (rule subgroupI) auto


856 


857 
lemma (in group) subgroup_imp_group:


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


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


860 


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


862 
"monoid G"


863 
by (rule monoid.intro)


864 


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


877 


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

14693

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

14551

894 
with subgr [THEN subgroup.m_closed]


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


896 
qed


897 


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


936 

14693

937 
end
