14551

1 
(*


2 
Title: Orders and Lattices


3 
Id: $Id$


4 
Author: Clemens Ballarin, started 7 November 2003


5 
Copyright: Clemens Ballarin


6 
*)


7 


8 
theory Lattice = Group:


9 


10 
section {* Order and Lattices *}


11 


12 
subsection {* Partial Orders *}


13 


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


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


16 


17 
locale order_syntax = struct L


18 


19 
locale partial_order = order_syntax +


20 
assumes refl [intro, simp]:


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


22 
and anti_sym [intro]:


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


24 
and trans [trans]:


25 
"[ x \<sqsubseteq> y; y \<sqsubseteq> z;


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


27 


28 
constdefs


29 
less :: "[('a, 'm) order_scheme, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)


30 
"less L x y == le L x y & x ~= y"


31 


32 
(* Upper and lower bounds of a set. *)


33 
Upper :: "[('a, 'm) order_scheme, 'a set] => 'a set"


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


35 
carrier L"


36 


37 
Lower :: "[('a, 'm) order_scheme, 'a set] => 'a set"


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


39 
carrier L"


40 


41 
(* Least and greatest, as predicate. *)


42 
least :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"


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


44 


45 
greatest :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"


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


47 


48 
(* Supremum and infimum *)


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


50 
"sup L A == THE x. least L x (Upper L A)"


51 


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


53 
"inf L A == THE x. greatest L x (Lower L A)"


54 


55 
join :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)


56 
"join L x y == sup L {x, y}"


57 


58 
meet :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)


59 
"meet L x y == inf L {x, y}"


60 


61 
(* Upper *)


62 


63 
lemma Upper_closed [intro, simp]:


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


65 
by (unfold Upper_def) clarify


66 


67 
lemma UpperD [dest]:


68 
includes order_syntax


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


70 
by (unfold Upper_def) blast


71 


72 
lemma Upper_memI:


73 
includes order_syntax


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


75 
by (unfold Upper_def) blast


76 


77 
lemma Upper_antimono:


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


79 
by (unfold Upper_def) blast


80 


81 
(* Lower *)


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


88 
includes order_syntax


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


90 
by (unfold Lower_def) blast


91 


92 
lemma Lower_memI:


93 
includes order_syntax


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


95 
by (unfold Lower_def) blast


96 


97 
lemma Lower_antimono:


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


99 
by (unfold Lower_def) blast


100 


101 
(* least *)


102 


103 
lemma least_carrier [intro, simp]:


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


105 
by (unfold least_def) fast


106 


107 
lemma least_mem:


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


109 
by (unfold least_def) fast


110 


111 
lemma (in partial_order) least_unique:


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


113 
by (unfold least_def) blast


114 


115 
lemma least_le:


116 
includes order_syntax


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


118 
by (unfold least_def) fast


119 


120 
lemma least_UpperI:


121 
includes order_syntax


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


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


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


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


126 
proof (unfold least_def, intro conjI)


127 
show "Upper L A \<subseteq> carrier L" by simp


128 
next


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


130 
next


131 
from below show "ALL x : Upper L A. s \<sqsubseteq> x" by fast


132 
qed


133 


134 
(* greatest *)


135 


136 
lemma greatest_carrier [intro, simp]:


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


138 
by (unfold greatest_def) fast


139 


140 
lemma greatest_mem:


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


142 
by (unfold greatest_def) fast


143 


144 
lemma (in partial_order) greatest_unique:


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


146 
by (unfold greatest_def) blast


147 


148 
lemma greatest_le:


149 
includes order_syntax


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


151 
by (unfold greatest_def) fast


152 


153 
lemma greatest_LowerI:


154 
includes order_syntax


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


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


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


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


159 
proof (unfold greatest_def, intro conjI)


160 
show "Lower L A \<subseteq> carrier L" by simp


161 
next


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


163 
next


164 
from above show "ALL x : Lower L A. x \<sqsubseteq> i" by fast


165 
qed


166 


167 
subsection {* Lattices *}


168 


169 
locale lattice = partial_order +


170 
assumes sup_of_two_exists:


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


172 
and inf_of_two_exists:


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


174 


175 
lemma least_Upper_above:


176 
includes order_syntax


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


178 
by (unfold least_def) blast


179 


180 
lemma greatest_Lower_above:


181 
includes order_syntax


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


183 
by (unfold greatest_def) blast


184 


185 
subsubsection {* Supremum *}


186 


187 
lemma (in lattice) joinI:


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


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


190 
proof (unfold join_def sup_def)


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


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


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


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


195 
by (fast intro: theI2 least_unique P)


196 
qed


197 


198 
lemma (in lattice) join_closed [simp]:


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


200 
by (rule joinI) (rule least_carrier)


201 


202 
lemma (in partial_order) sup_of_singletonI:


203 
(* only reflexivity needed ? *)


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


205 
by (rule least_UpperI) fast+


206 


207 
lemma (in partial_order) sup_of_singleton [simp]:


208 
includes order_syntax


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


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


211 


212 
text {* Condition on A: supremum exists. *}


213 


214 
lemma (in lattice) sup_insertI:


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


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


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


218 
proof (unfold sup_def)


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


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


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


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


223 
from L sup_of_two_exists least_a


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


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


226 
proof (rule theI2 [where a = s])


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


228 
proof (rule least_UpperI)


229 
fix z


230 
assume xA: "z \<in> insert x A"


231 
show "z \<sqsubseteq> s"


232 
proof 


233 
{


234 
assume "z = x" then have ?thesis


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


236 
}


237 
moreover


238 
{


239 
assume "z \<in> A"


240 
with L least_s least_a have ?thesis


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


242 
}


243 
moreover note xA


244 
ultimately show ?thesis by blast


245 
qed


246 
next


247 
fix y


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


249 
show "s \<sqsubseteq> y"


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


251 
fix z


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


253 
show "z \<sqsubseteq> y"


254 
proof 


255 
{


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 have ?thesis by (fast dest: least_le)


262 
}


263 
moreover


264 
{


265 
assume "z = x"


266 
with y L have ?thesis by blast


267 
}


268 
moreover note z


269 
ultimately show ?thesis by blast


270 
qed


271 
qed (rule Upper_closed [THEN subsetD])


272 
next


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


274 
next


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


276 
qed


277 
next


278 
fix l


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


280 
show "l = s"


281 
proof (rule least_unique)


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


283 
proof (rule least_UpperI)


284 
fix z


285 
assume xA: "z \<in> insert x A"


286 
show "z \<sqsubseteq> s"


287 
proof 


288 
{


289 
assume "z = x" then have ?thesis


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


291 
}


292 
moreover


293 
{


294 
assume "z \<in> A"


295 
with L least_s least_a have ?thesis


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


297 
}


298 
moreover note xA


299 
ultimately show ?thesis by blast


300 
qed


301 
next


302 
fix y


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


304 
show "s \<sqsubseteq> y"


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


306 
fix z


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


308 
show "z \<sqsubseteq> y"


309 
proof 


310 
{


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


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


313 
apply (rule Upper_antimono) apply clarify apply assumption


314 
done


315 
assume "z = a"


316 
with y' least_a have ?thesis by (fast dest: least_le)


317 
}


318 
moreover


319 
{


320 
assume "z = x"


321 
with y L have ?thesis by blast


322 
}


323 
moreover note z


324 
ultimately show ?thesis by blast


325 
qed


326 
qed (rule Upper_closed [THEN subsetD])


327 
next


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


329 
next


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


331 
qed


332 
qed


333 
qed


334 
qed


335 


336 
lemma (in lattice) finite_sup_least:


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


338 
proof (induct set: Finites)


339 
case empty then show ?case by simp


340 
next


341 
case (insert A x)


342 
show ?case


343 
proof (cases "A = {}")


344 
case True


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


346 
next


347 
case False


348 
from insert show ?thesis


349 
proof (rule_tac sup_insertI)


350 
from False insert show "least L (\<Squnion> A) (Upper L A)" by simp


351 
qed simp_all


352 
qed


353 
qed


354 


355 
lemma (in lattice) finite_sup_insertI:


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


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


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


359 
proof (cases "A = {}")


360 
case True with P and xA show ?thesis


361 
by (simp add: sup_of_singletonI)


362 
next


363 
case False with P and xA show ?thesis


364 
by (simp add: sup_insertI finite_sup_least)


365 
qed


366 


367 
lemma (in lattice) finite_sup_closed:


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


369 
proof (induct set: Finites)


370 
case empty then show ?case by simp


371 
next


372 
case (insert A x) then show ?case


373 
by (rule_tac finite_sup_insertI) (simp_all)


374 
qed


375 


376 
lemma (in lattice) join_left:


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


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


379 


380 
lemma (in lattice) join_right:


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


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


383 


384 
lemma (in lattice) sup_of_two_least:


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


386 
proof (unfold sup_def)


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


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


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


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


391 
qed


392 


393 
lemma (in lattice) join_le:


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


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


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


397 
proof (rule joinI)


398 
fix s


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


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


401 
qed


402 


403 
lemma (in lattice) join_assoc_lemma:


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


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


406 
proof (rule finite_sup_insertI)


407 
(* The textbook argument in Jacobson I, p 457 *)


408 
fix s


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


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


411 
proof (rule anti_sym)


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


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


414 
next


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


416 
by (erule_tac least_le)


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


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


419 
qed (simp_all add: L)


420 


421 
lemma join_comm:


422 
includes order_syntax


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


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


425 


426 
lemma (in lattice) join_assoc:


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


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


429 
proof 


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


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


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


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


434 
finally show ?thesis .


435 
qed


436 


437 
subsubsection {* Infimum *}


438 


439 
lemma (in lattice) meetI:


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


441 
x \<in> carrier L; y \<in> carrier L ]


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


443 
proof (unfold meet_def inf_def)


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


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


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


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


448 
by (fast intro: theI2 greatest_unique P)


449 
qed


450 


451 
lemma (in lattice) meet_closed [simp]:


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


453 
by (rule meetI) (rule greatest_carrier)


454 


455 
lemma (in partial_order) inf_of_singletonI:


456 
(* only reflexivity needed ? *)


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


458 
by (rule greatest_LowerI) fast+


459 


460 
lemma (in partial_order) inf_of_singleton [simp]:


461 
includes order_syntax


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


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


464 


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


466 


467 
lemma (in lattice) inf_insertI:


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


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


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


471 
proof (unfold inf_def)


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


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


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


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


476 
from L inf_of_two_exists greatest_a


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


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


479 
proof (rule theI2 [where a = i])


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


481 
proof (rule greatest_LowerI)


482 
fix z


483 
assume xA: "z \<in> insert x A"


484 
show "i \<sqsubseteq> z"


485 
proof 


486 
{


487 
assume "z = x" then have ?thesis


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


489 
}


490 
moreover


491 
{


492 
assume "z \<in> A"


493 
with L greatest_i greatest_a have ?thesis


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


495 
}


496 
moreover note xA


497 
ultimately show ?thesis by blast


498 
qed


499 
next


500 
fix y


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


502 
show "y \<sqsubseteq> i"


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


504 
fix z


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


506 
show "y \<sqsubseteq> z"


507 
proof 


508 
{


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


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


511 
apply (rule Lower_antimono) apply clarify apply assumption


512 
done


513 
assume "z = a"


514 
with y' greatest_a have ?thesis by (fast dest: greatest_le)


515 
}


516 
moreover


517 
{


518 
assume "z = x"


519 
with y L have ?thesis by blast


520 
}


521 
moreover note z


522 
ultimately show ?thesis by blast


523 
qed


524 
qed (rule Lower_closed [THEN subsetD])


525 
next


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


527 
next


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


529 
qed


530 
next


531 
fix g


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


533 
show "g = i"


534 
proof (rule greatest_unique)


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


536 
proof (rule greatest_LowerI)


537 
fix z


538 
assume xA: "z \<in> insert x A"


539 
show "i \<sqsubseteq> z"


540 
proof 


541 
{


542 
assume "z = x" then have ?thesis


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


544 
}


545 
moreover


546 
{


547 
assume "z \<in> A"


548 
with L greatest_i greatest_a have ?thesis


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


550 
}


551 
moreover note xA


552 
ultimately show ?thesis by blast


553 
qed


554 
next


555 
fix y


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


557 
show "y \<sqsubseteq> i"


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


559 
fix z


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


561 
show "y \<sqsubseteq> z"


562 
proof 


563 
{


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


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


566 
apply (rule Lower_antimono) apply clarify apply assumption


567 
done


568 
assume "z = a"


569 
with y' greatest_a have ?thesis by (fast dest: greatest_le)


570 
}


571 
moreover


572 
{


573 
assume "z = x"


574 
with y L have ?thesis by blast


575 
}


576 
moreover note z


577 
ultimately show ?thesis by blast


578 
qed


579 
qed (rule Lower_closed [THEN subsetD])


580 
next


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


582 
next


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


584 
qed


585 
qed


586 
qed


587 
qed


588 


589 
lemma (in lattice) finite_inf_greatest:


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


591 
proof (induct set: Finites)


592 
case empty then show ?case by simp


593 
next


594 
case (insert A x)


595 
show ?case


596 
proof (cases "A = {}")


597 
case True


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


599 
next


600 
case False


601 
from insert show ?thesis


602 
proof (rule_tac inf_insertI)


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


604 
qed simp_all


605 
qed


606 
qed


607 


608 
lemma (in lattice) finite_inf_insertI:


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


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


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


612 
proof (cases "A = {}")


613 
case True with P and xA show ?thesis


614 
by (simp add: inf_of_singletonI)


615 
next


616 
case False with P and xA show ?thesis


617 
by (simp add: inf_insertI finite_inf_greatest)


618 
qed


619 


620 
lemma (in lattice) finite_inf_closed:


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


622 
proof (induct set: Finites)


623 
case empty then show ?case by simp


624 
next


625 
case (insert A x) then show ?case


626 
by (rule_tac finite_inf_insertI) (simp_all)


627 
qed


628 


629 
lemma (in lattice) meet_left:


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


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


632 


633 
lemma (in lattice) meet_right:


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


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


636 


637 
lemma (in lattice) inf_of_two_greatest:


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


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


640 
proof (unfold inf_def)


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


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


643 
with L


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


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


646 
qed


647 


648 
lemma (in lattice) meet_le:


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


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


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


652 
proof (rule meetI)


653 
fix i


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


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


656 
qed


657 


658 
lemma (in lattice) meet_assoc_lemma:


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


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


661 
proof (rule finite_inf_insertI)


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


663 
fix i


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


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


666 
proof (rule anti_sym)


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


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


669 
next


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


671 
by (erule_tac greatest_le)


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


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


674 
qed (simp_all add: L)


675 


676 
lemma meet_comm:


677 
includes order_syntax


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


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


680 


681 
lemma (in lattice) meet_assoc:


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


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


684 
proof 


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


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


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


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


689 
finally show ?thesis .


690 
qed


691 


692 
subsection {* Total Orders *}


693 


694 
locale total_order = lattice +


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


696 


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


698 


699 
lemma (in partial_order) total_orderI:


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


701 
shows "total_order L"


702 
proof (rule total_order.intro)


703 
show "lattice_axioms L"


704 
proof (rule lattice_axioms.intro)


705 
fix x y


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


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


708 
proof 


709 
note total L


710 
moreover


711 
{


712 
assume "x \<sqsubseteq> y"


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


714 
by (rule_tac least_UpperI) auto


715 
}


716 
moreover


717 
{


718 
assume "y \<sqsubseteq> x"


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


720 
by (rule_tac least_UpperI) auto


721 
}


722 
ultimately show ?thesis by blast


723 
qed


724 
next


725 
fix x y


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


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


728 
proof 


729 
note total L


730 
moreover


731 
{


732 
assume "y \<sqsubseteq> x"


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


734 
by (rule_tac greatest_LowerI) auto


735 
}


736 
moreover


737 
{


738 
assume "x \<sqsubseteq> y"


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


740 
by (rule_tac greatest_LowerI) auto


741 
}


742 
ultimately show ?thesis by blast


743 
qed


744 
qed


745 
qed (assumption  rule total_order_axioms.intro)+


746 


747 
subsection {* Complete lattices *}


748 


749 
locale complete_lattice = lattice +


750 
assumes sup_exists:


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


752 
and inf_exists:


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


754 


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


756 


757 
lemma (in partial_order) complete_latticeI:


758 
assumes sup_exists:


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


760 
and inf_exists:


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


762 
shows "complete_lattice L"


763 
proof (rule complete_lattice.intro)


764 
show "lattice_axioms L"


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


766 
qed (assumption  rule complete_lattice_axioms.intro)+


767 


768 
constdefs


769 
top :: "('a, 'm) order_scheme => 'a" ("\<top>\<index>")


770 
"top L == sup L (carrier L)"


771 


772 
bottom :: "('a, 'm) order_scheme => 'a" ("\<bottom>\<index>")


773 
"bottom L == inf L (carrier L)"


774 


775 


776 
lemma (in complete_lattice) supI:


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


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


779 
proof (unfold sup_def)


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


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


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


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


784 
by (fast intro: theI2 least_unique P)


785 
qed


786 


787 
lemma (in complete_lattice) sup_closed [simp]:


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


789 
by (rule supI) simp_all


790 


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


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


793 
by (unfold top_def) simp


794 


795 
lemma (in complete_lattice) infI:


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


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


798 
proof (unfold inf_def)


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


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


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


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


803 
by (fast intro: theI2 greatest_unique P)


804 
qed


805 


806 
lemma (in complete_lattice) inf_closed [simp]:


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


808 
by (rule infI) simp_all


809 


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


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


812 
by (unfold bottom_def) simp


813 


814 
text {* Jacobson: Theorem 8.1 *}


815 


816 
lemma Lower_empty [simp]:


817 
"Lower L {} = carrier L"


818 
by (unfold Lower_def) simp


819 


820 
lemma Upper_empty [simp]:


821 
"Upper L {} = carrier L"


822 
by (unfold Upper_def) simp


823 


824 
theorem (in partial_order) complete_lattice_criterion1:


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


826 
and inf_exists:


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


828 
shows "complete_lattice L"


829 
proof (rule complete_latticeI)


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


831 
fix A


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


833 
let ?B = "Upper L A"


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


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


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


837 
from inf_exists [OF B_L B_non_empty]


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


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


840 
apply (rule least_UpperI)


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


842 
apply (rule b_inf_B)


843 
apply (rule Lower_memI)


844 
apply (erule UpperD)


845 
apply assumption


846 
apply (rule L)


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


848 
apply (erule greatest_Lower_above [OF b_inf_B])


849 
apply simp


850 
apply (rule L)


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


852 
done


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


854 
next


855 
fix A


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


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


858 
proof (cases "A = {}")


859 
case True then show ?thesis


860 
by (simp add: top_exists)


861 
next


862 
case False with L show ?thesis


863 
by (rule inf_exists)


864 
qed


865 
qed


866 


867 
(* TODO: prove dual version *)


868 


869 
subsection {* Examples *}


870 


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


872 


873 
theorem powerset_is_complete_lattice:


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


875 
(is "complete_lattice ?L")


876 
proof (rule partial_order.complete_latticeI)


877 
show "partial_order ?L"


878 
by (rule partial_order.intro) auto


879 
next


880 
fix B


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


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


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


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


885 
next


886 
fix B


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


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


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


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


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


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


893 
qed


894 


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


896 


897 
theorem (in group) subgroups_partial_order:


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


899 
by (rule partial_order.intro) simp_all


900 


901 
lemma (in group) subgroup_self:


902 
"subgroup (carrier G) G"


903 
by (rule subgroupI) auto


904 


905 
lemma (in group) subgroup_imp_group:


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


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


908 


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


910 
"monoid G"


911 
by (rule monoid.intro)


912 


913 
lemma (in group) subgroup_inv_equality:


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


915 
apply (rule_tac inv_equality [THEN sym])


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


917 
apply assumption+


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


919 
apply assumption+


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


921 
apply assumption


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


923 
apply assumption+


924 
done


925 


926 
theorem (in group) subgroups_Inter:


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


928 
and not_empty: "A ~= {}"


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


930 
proof (rule subgroupI)


931 
from subgr [THEN subgroup.subset] and not_empty


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


933 
next


934 
from subgr [THEN subgroup.one_closed]


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


936 
next


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


938 
with subgr [THEN subgroup.m_inv_closed]


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


940 
next


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


942 
with subgr [THEN subgroup.m_closed]


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


944 
qed


945 


946 
theorem (in group) subgroups_complete_lattice:


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


948 
(is "complete_lattice ?L")


949 
proof (rule partial_order.complete_lattice_criterion1)


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


951 
next


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


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


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


955 
next


956 
fix A


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


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


959 
by (fastsimp intro: subgroups_Inter)


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


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


962 
proof (rule greatest_LowerI)


963 
fix H


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


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


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


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


968 
by (rule subgroup_imp_group)


969 
from groupH have monoidH: "monoid ?H"


970 
by (rule group.is_monoid)


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


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


973 
next


974 
fix H


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


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


977 
next


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


979 
next


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


981 
qed


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


983 
qed


984 


985 
end 