(* Title: HOL/Lattice/Lattice.thy
Author: Markus Wenzel, TU Muenchen
*)
header {* Lattices *}
theory Lattice imports Bounds begin
subsection {* Lattice operations *}
text {*
A \emph{lattice} is a partial order with infimum and supremum of any
two elements (thus any \emph{finite} number of elements have bounds
as well).
*}
class lattice =
assumes ex_inf: "\inf. is_inf x y inf"
assumes ex_sup: "\sup. is_sup x y sup"
text {*
The @{text \} (meet) and @{text \} (join) operations select such
infimum and supremum elements.
*}
definition
meet :: "'a::lattice \ 'a \ 'a" (infixl "&&" 70) where
"x && y = (THE inf. is_inf x y inf)"
definition
join :: "'a::lattice \ 'a \ 'a" (infixl "||" 65) where
"x || y = (THE sup. is_sup x y sup)"
notation (xsymbols)
meet (infixl "\" 70) and
join (infixl "\" 65)
text {*
Due to unique existence of bounds, the lattice operations may be
exhibited as follows.
*}
lemma meet_equality [elim?]: "is_inf x y inf \ x \ y = inf"
proof (unfold meet_def)
assume "is_inf x y inf"
then show "(THE inf. is_inf x y inf) = inf"
by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`])
qed
lemma meetI [intro?]:
"inf \ x \ inf \ y \ (\z. z \ x \ z \ y \ z \ inf) \ x \ y = inf"
by (rule meet_equality, rule is_infI) blast+
lemma join_equality [elim?]: "is_sup x y sup \ x \ y = sup"
proof (unfold join_def)
assume "is_sup x y sup"
then show "(THE sup. is_sup x y sup) = sup"
by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`])
qed
lemma joinI [intro?]: "x \ sup \ y \ sup \
(\z. x \ z \ y \ z \ sup \ z) \ x \ y = sup"
by (rule join_equality, rule is_supI) blast+
text {*
\medskip The @{text \} and @{text \} operations indeed determine
bounds on a lattice structure.
*}
lemma is_inf_meet [intro?]: "is_inf x y (x \ y)"
proof (unfold meet_def)
from ex_inf obtain inf where "is_inf x y inf" ..
then show "is_inf x y (THE inf. is_inf x y inf)"
by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`])
qed
lemma meet_greatest [intro?]: "z \ x \ z \ y \ z \ x \ y"
by (rule is_inf_greatest) (rule is_inf_meet)
lemma meet_lower1 [intro?]: "x \ y \ x"
by (rule is_inf_lower) (rule is_inf_meet)
lemma meet_lower2 [intro?]: "x \ y \ y"
by (rule is_inf_lower) (rule is_inf_meet)
lemma is_sup_join [intro?]: "is_sup x y (x \ y)"
proof (unfold join_def)
from ex_sup obtain sup where "is_sup x y sup" ..
then show "is_sup x y (THE sup. is_sup x y sup)"
by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`])
qed
lemma join_least [intro?]: "x \ z \ y \ z \ x \ y \ z"
by (rule is_sup_least) (rule is_sup_join)
lemma join_upper1 [intro?]: "x \ x \ y"
by (rule is_sup_upper) (rule is_sup_join)
lemma join_upper2 [intro?]: "y \ x \ y"
by (rule is_sup_upper) (rule is_sup_join)
subsection {* Duality *}
text {*
The class of lattices is closed under formation of dual structures.
This means that for any theorem of lattice theory, the dualized
statement holds as well; this important fact simplifies many proofs
of lattice theory.
*}
instance dual :: (lattice) lattice
proof
fix x' y' :: "'a::lattice dual"
show "\inf'. is_inf x' y' inf'"
proof -
have "\sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
then have "\sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
by (simp only: dual_inf)
then show ?thesis by (simp add: dual_ex [symmetric])
qed
show "\sup'. is_sup x' y' sup'"
proof -
have "\inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
then have "\inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
by (simp only: dual_sup)
then show ?thesis by (simp add: dual_ex [symmetric])
qed
qed
text {*
Apparently, the @{text \} and @{text \} operations are dual to each
other.
*}
theorem dual_meet [intro?]: "dual (x \ y) = dual x \ dual y"
proof -
from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \ y))" ..
then have "dual x \ dual y = dual (x \ y)" ..
then show ?thesis ..
qed
theorem dual_join [intro?]: "dual (x \ y) = dual x \ dual y"
proof -
from is_sup_join have "is_inf (dual x) (dual y) (dual (x \ y))" ..
then have "dual x \ dual y = dual (x \ y)" ..
then show ?thesis ..
qed
subsection {* Algebraic properties \label{sec:lattice-algebra} *}
text {*
The @{text \} and @{text \} operations have the following
characteristic algebraic properties: associative (A), commutative
(C), and absorptive (AB).
*}
theorem meet_assoc: "(x \ y) \ z = x \ (y \ z)"
proof
show "x \ (y \ z) \ x \ y"
proof
show "x \ (y \ z) \ x" ..
show "x \ (y \ z) \ y"
proof -
have "x \ (y \ z) \ y \ z" ..
also have "\ \ y" ..
finally show ?thesis .
qed
qed
show "x \ (y \ z) \ z"
proof -
have "x \ (y \ z) \ y \ z" ..
also have "\ \ z" ..
finally show ?thesis .
qed
fix w assume "w \ x \ y" and "w \ z"
show "w \ x \ (y \ z)"
proof
show "w \ x"
proof -
have "w \ x \ y" by fact
also have "\ \ x" ..
finally show ?thesis .
qed
show "w \ y \ z"
proof
show "w \ y"
proof -
have "w \ x \ y" by fact
also have "\ \ y" ..
finally show ?thesis .
qed
show "w \ z" by fact
qed
qed
qed
theorem join_assoc: "(x \ y) \ z = x \ (y \ z)"
proof -
have "dual ((x \ y) \ z) = (dual x \ dual y) \ dual z"
by (simp only: dual_join)
also have "\ = dual x \ (dual y \ dual z)"
by (rule meet_assoc)
also have "\ = dual (x \ (y \ z))"
by (simp only: dual_join)
finally show ?thesis ..
qed
theorem meet_commute: "x \ y = y \ x"
proof
show "y \ x \ x" ..
show "y \ x \ y" ..
fix z assume "z \ y" and "z \ x"
then show "z \ y \ x" ..
qed
theorem join_commute: "x \ y = y \ x"
proof -
have "dual (x \ y) = dual x \ dual y" ..
also have "\ = dual y \ dual x"
by (rule meet_commute)
also have "\ = dual (y \ x)"
by (simp only: dual_join)
finally show ?thesis ..
qed
theorem meet_join_absorb: "x \ (x \ y) = x"
proof
show "x \ x" ..
show "x \ x \ y" ..
fix z assume "z \ x" and "z \ x \ y"
show "z \ x" by fact
qed
theorem join_meet_absorb: "x \ (x \ y) = x"
proof -
have "dual x \ (dual x \ dual y) = dual x"
by (rule meet_join_absorb)
then have "dual (x \ (x \ y)) = dual x"
by (simp only: dual_meet dual_join)
then show ?thesis ..
qed
text {*
\medskip Some further algebraic properties hold as well. The
property idempotent (I) is a basic algebraic consequence of (AB).
*}
theorem meet_idem: "x \ x = x"
proof -
have "x \ (x \ (x \ x)) = x" by (rule meet_join_absorb)
also have "x \ (x \ x) = x" by (rule join_meet_absorb)
finally show ?thesis .
qed
theorem join_idem: "x \ x = x"
proof -
have "dual x \ dual x = dual x"
by (rule meet_idem)
then have "dual (x \ x) = dual x"
by (simp only: dual_join)
then show ?thesis ..
qed
text {*
Meet and join are trivial for related elements.
*}
theorem meet_related [elim?]: "x \ y \ x \ y = x"
proof
assume "x \ y"
show "x \ x" ..
show "x \ y" by fact
fix z assume "z \ x" and "z \ y"
show "z \ x" by fact
qed
theorem join_related [elim?]: "x \ y \ x \ y = y"
proof -
assume "x \ y" then have "dual y \ dual x" ..
then have "dual y \ dual x = dual y" by (rule meet_related)
also have "dual y \ dual x = dual (y \ x)" by (simp only: dual_join)
also have "y \ x = x \ y" by (rule join_commute)
finally show ?thesis ..
qed
subsection {* Order versus algebraic structure *}
text {*
The @{text \} and @{text \} operations are connected with the
underlying @{text \} relation in a canonical manner.
*}
theorem meet_connection: "(x \ y) = (x \ y = x)"
proof
assume "x \ y"
then have "is_inf x y x" ..
then show "x \ y = x" ..
next
have "x \ y \ y" ..
also assume "x \ y = x"
finally show "x \ y" .
qed
theorem join_connection: "(x \ y) = (x \ y = y)"
proof
assume "x \ y"
then have "is_sup x y y" ..
then show "x \ y = y" ..
next
have "x \ x \ y" ..
also assume "x \ y = y"
finally show "x \ y" .
qed
text {*
\medskip The most fundamental result of the meta-theory of lattices
is as follows (we do not prove it here).
Given a structure with binary operations @{text \} and @{text \}
such that (A), (C), and (AB) hold (cf.\
\S\ref{sec:lattice-algebra}). This structure represents a lattice,
if the relation @{term "x \ y"} is defined as @{term "x \ y = x"}
(alternatively as @{term "x \ y = y"}). Furthermore, infimum and
supremum with respect to this ordering coincide with the original
@{text \} and @{text \} operations.
*}
subsection {* Example instances *}
subsubsection {* Linear orders *}
text {*
Linear orders with @{term minimum} and @{term maximum} operations
are a (degenerate) example of lattice structures.
*}
definition
minimum :: "'a::linear_order \ 'a \ 'a" where
"minimum x y = (if x \ y then x else y)"
definition
maximum :: "'a::linear_order \ 'a \ 'a" where
"maximum x y = (if x \ y then y else x)"
lemma is_inf_minimum: "is_inf x y (minimum x y)"
proof
let ?min = "minimum x y"
from leq_linear show "?min \ x" by (auto simp add: minimum_def)
from leq_linear show "?min \ y" by (auto simp add: minimum_def)
fix z assume "z \ x" and "z \ y"
with leq_linear show "z \ ?min" by (auto simp add: minimum_def)
qed
lemma is_sup_maximum: "is_sup x y (maximum x y)" (* FIXME dualize!? *)
proof
let ?max = "maximum x y"
from leq_linear show "x \ ?max" by (auto simp add: maximum_def)
from leq_linear show "y \ ?max" by (auto simp add: maximum_def)
fix z assume "x \ z" and "y \ z"
with leq_linear show "?max \ z" by (auto simp add: maximum_def)
qed
instance linear_order \ lattice
proof
fix x y :: "'a::linear_order"
from is_inf_minimum show "\inf. is_inf x y inf" ..
from is_sup_maximum show "\sup. is_sup x y sup" ..
qed
text {*
The lattice operations on linear orders indeed coincide with @{term
minimum} and @{term maximum}.
*}
theorem meet_mimimum: "x \ y = minimum x y"
by (rule meet_equality) (rule is_inf_minimum)
theorem meet_maximum: "x \ y = maximum x y"
by (rule join_equality) (rule is_sup_maximum)
subsubsection {* Binary products *}
text {*
The class of lattices is closed under direct binary products (cf.\
\S\ref{sec:prod-order}).
*}
lemma is_inf_prod: "is_inf p q (fst p \ fst q, snd p \ snd q)"
proof
show "(fst p \ fst q, snd p \