# Theory Lattice

(*  Title:      HOL/Lattice/Lattice.thy
Author:     Markus Wenzel, TU Muenchen
*)

section ‹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 ‹⊓› (meet) and ‹⊔› (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)"

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 ‹⊓› and ‹⊔› 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 ‹⊓› and ‹⊔› 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 ‹⊓› and ‹⊔› 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 ‹⊓› and ‹⊔› operations are connected with the
underlying ‹⊑› 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 ‹⊓› and ‹⊔›
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
‹⊓› and ‹⊔› 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 ⊓ snd q) ⊑ p"
proof -
have "fst p ⊓ fst q ⊑ fst p" ..
moreover have "snd p ⊓ snd q ⊑ snd p" ..
ultimately show ?thesis by (simp add: leq_prod_def)
qed
show "(fst p ⊓ fst q, snd p ⊓ snd q) ⊑ q"
proof -
have "fst p ⊓ fst q ⊑ fst q" ..
moreover have "snd p ⊓ snd q ⊑ snd q" ..
ultimately show ?thesis by (simp add: leq_prod_def)
qed
fix r assume rp: "r ⊑ p" and rq: "r ⊑ q"
show "r ⊑ (fst p ⊓ fst q, snd p ⊓ snd q)"
proof -
have "fst r ⊑ fst p ⊓ fst q"
proof
from rp show "fst r ⊑ fst p" by (simp add: leq_prod_def)
from rq show "fst r ⊑ fst q" by (simp add: leq_prod_def)
qed
moreover have "snd r ⊑ snd p ⊓ snd q"
proof
from rp show "snd r ⊑ snd p" by (simp add: leq_prod_def)
from rq show "snd r ⊑ snd q" by (simp add: leq_prod_def)
qed
ultimately show ?thesis by (simp add: leq_prod_def)
qed
qed

lemma is_sup_prod: "is_sup p q (fst p ⊔ fst q, snd p ⊔ snd q)"  (* FIXME dualize!? *)
proof
show "p ⊑ (fst p ⊔ fst q, snd p ⊔ snd q)"
proof -
have "fst p ⊑ fst p ⊔ fst q" ..
moreover have "snd p ⊑ snd p ⊔ snd q" ..
ultimately show ?thesis by (simp add: leq_prod_def)
qed
show "q ⊑ (fst p ⊔ fst q, snd p ⊔ snd q)"
proof -
have "fst q ⊑ fst p ⊔ fst q" ..
moreover have "snd q ⊑ snd p ⊔ snd q" ..
ultimately show ?thesis by (simp add: leq_prod_def)
qed
fix r assume "pr": "p ⊑ r" and qr: "q ⊑ r"
show "(fst p ⊔ fst q, snd p ⊔ snd q) ⊑ r"
proof -
have "fst p ⊔ fst q ⊑ fst r"
proof
from "pr" show "fst p ⊑ fst r" by (simp add: leq_prod_def)
from qr show "fst q ⊑ fst r" by (simp add: leq_prod_def)
qed
moreover have "snd p ⊔ snd q ⊑ snd r"
proof
from "pr" show "snd p ⊑ snd r" by (simp add: leq_prod_def)
from qr show "snd q ⊑ snd r" by (simp add: leq_prod_def)
qed
ultimately show ?thesis by (simp add: leq_prod_def)
qed
qed

instance prod :: (lattice, lattice) lattice
proof
fix p q :: "'a::lattice × 'b::lattice"
from is_inf_prod show "∃inf. is_inf p q inf" ..
from is_sup_prod show "∃sup. is_sup p q sup" ..
qed

text ‹
The lattice operations on a binary product structure indeed coincide
with the products of the original ones.
›

theorem meet_prod: "p ⊓ q = (fst p ⊓ fst q, snd p ⊓ snd q)"
by (rule meet_equality) (rule is_inf_prod)

theorem join_prod: "p ⊔ q = (fst p ⊔ fst q, snd p ⊔ snd q)"
by (rule join_equality) (rule is_sup_prod)

subsubsection ‹General products›

text ‹
The class of lattices is closed under general products (function
spaces) as well (cf.\ \S\ref{sec:fun-order}).
›

lemma is_inf_fun: "is_inf f g (λx. f x ⊓ g x)"
proof
show "(λx. f x ⊓ g x) ⊑ f"
proof
fix x show "f x ⊓ g x ⊑ f x" ..
qed
show "(λx. f x ⊓ g x) ⊑ g"
proof
fix x show "f x ⊓ g x ⊑ g x" ..
qed
fix h assume hf: "h ⊑ f" and hg: "h ⊑ g"
show "h ⊑ (λx. f x ⊓ g x)"
proof
fix x
show "h x ⊑ f x ⊓ g x"
proof
from hf show "h x ⊑ f x" ..
from hg show "h x ⊑ g x" ..
qed
qed
qed

lemma is_sup_fun: "is_sup f g (λx. f x ⊔ g x)"   (* FIXME dualize!? *)
proof
show "f ⊑ (λx. f x ⊔ g x)"
proof
fix x show "f x ⊑ f x ⊔ g x" ..
qed
show "g ⊑ (λx. f x ⊔ g x)"
proof
fix x show "g x ⊑ f x ⊔ g x" ..
qed
fix h assume fh: "f ⊑ h" and gh: "g ⊑ h"
show "(λx. f x ⊔ g x) ⊑ h"
proof
fix x
show "f x ⊔ g x ⊑ h x"
proof
from fh show "f x ⊑ h x" ..
from gh show "g x ⊑ h x" ..
qed
qed
qed

instance "fun" :: (type, lattice) lattice
proof
fix f g :: "'a ⇒ 'b::lattice"
show "∃inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from … show … .."} does not work!? unification incompleteness!? *)
show "∃sup. is_sup f g sup" by rule (rule is_sup_fun)
qed

text ‹
The lattice operations on a general product structure (function
space) indeed emerge by point-wise lifting of the original ones.
›

theorem meet_fun: "f ⊓ g = (λx. f x ⊓ g x)"
by (rule meet_equality) (rule is_inf_fun)

theorem join_fun: "f ⊔ g = (λx. f x ⊔ g x)"
by (rule join_equality) (rule is_sup_fun)

subsection ‹Monotonicity and semi-morphisms›

text ‹
The lattice operations are monotone in both argument positions.  In
fact, monotonicity of the second position is trivial due to
commutativity.
›

theorem meet_mono: "x ⊑ z ⟹ y ⊑ w ⟹ x ⊓ y ⊑ z ⊓ w"
proof -
{
fix a b c :: "'a::lattice"
assume "a ⊑ c" have "a ⊓ b ⊑ c ⊓ b"
proof
have "a ⊓ b ⊑ a" ..
also have "… ⊑ c" by fact
finally show "a ⊓ b ⊑ c" .
show "a ⊓ b ⊑ b" ..
qed
} note this [elim?]
assume "x ⊑ z" then have "x ⊓ y ⊑ z ⊓ y" ..
also have "… = y ⊓ z" by (rule meet_commute)
also assume "y ⊑ w" then have "y ⊓ z ⊑ w ⊓ z" ..
also have "… = z ⊓ w" by (rule meet_commute)
finally show ?thesis .
qed

theorem join_mono: "x ⊑ z ⟹ y ⊑ w ⟹ x ⊔ y ⊑ z ⊔ w"
proof -
assume "x ⊑ z" then have "dual z ⊑ dual x" ..
moreover assume "y ⊑ w" then have "dual w ⊑ dual y" ..
ultimately have "dual z ⊓ dual w ⊑ dual x ⊓ dual y"
by (rule meet_mono)
then have "dual (z ⊔ w) ⊑ dual (x ⊔ y)"
by (simp only: dual_join)
then show ?thesis ..
qed

text ‹
\medskip A semi-morphisms is a function ‹f› that preserves the
lattice operations in the following manner: \<^term>‹f (x ⊓ y) ⊑ f x
⊓ f y› and \<^term>‹f x ⊔ f y ⊑ f (x ⊔ y)›, respectively.  Any of
these properties is equivalent with monotonicity.
›

theorem meet_semimorph:
"(⋀x y. f (x ⊓ y) ⊑ f x ⊓ f y) ≡ (⋀x y. x ⊑ y ⟹ f x ⊑ f y)"
proof
assume morph: "⋀x y. f (x ⊓ y) ⊑ f x ⊓ f y"
fix x y :: "'a::lattice"
assume "x ⊑ y"
then have "x ⊓ y = x" ..
then have "x = x ⊓ y" ..
also have "f … ⊑ f x ⊓ f y" by (rule morph)
also have "… ⊑ f y" ..
finally show "f x ⊑ f y" .
next
assume mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y"
show "⋀x y. f (x ⊓ y) ⊑ f x ⊓ f y"
proof -
fix x y
show "f (x ⊓ y) ⊑ f x ⊓ f y"
proof
have "x ⊓ y ⊑ x" .. then show "f (x ⊓ y) ⊑ f x" by (rule mono)
have "x ⊓ y ⊑ y" .. then show "f (x ⊓ y) ⊑ f y" by (rule mono)
qed
qed
qed

lemma join_semimorph:
"(⋀x y. f x ⊔ f y ⊑ f (x ⊔ y)) ≡ (⋀x y. x ⊑ y ⟹ f x ⊑ f y)"
proof
assume morph: "⋀x y. f x ⊔ f y ⊑ f (x ⊔ y)"
fix x y :: "'a::lattice"
assume "x ⊑ y" then have "x ⊔ y = y" ..
have "f x ⊑ f x ⊔ f y" ..
also have "… ⊑ f (x ⊔ y)" by (rule morph)
also from ‹x ⊑ y› have "x ⊔ y = y" ..
finally show "f x ⊑ f y" .
next
assume mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y"
show "⋀x y. f x ⊔ f y ⊑ f (x ⊔ y)"
proof -
fix x y
show "f x ⊔ f y ⊑ f (x ⊔ y)"
proof
have "x ⊑ x ⊔ y" .. then show "f x ⊑ f (x ⊔ y)" by (rule mono)
have "y ⊑ x ⊔ y" .. then show "f y ⊑ f (x ⊔ y)" by (rule mono)
qed
qed
qed

end