Theory HOL-Lattice.CompleteLattice
section ‹Complete lattices›
theory CompleteLattice imports Lattice begin
subsection ‹Complete lattice operations›
text ‹
A \emph{complete lattice} is a partial order with general
(infinitary) infimum of any set of elements. General supremum
exists as well, as a consequence of the connection of infinitary
bounds (see \S\ref{sec:connect-bounds}).
›
class complete_lattice =
assumes ex_Inf: "∃inf. is_Inf A inf"
theorem ex_Sup: "∃sup::'a::complete_lattice. is_Sup A sup"
proof -
from ex_Inf obtain sup where "is_Inf {b. ∀a∈A. a ⊑ b} sup" by blast
then have "is_Sup A sup" by (rule Inf_Sup)
then show ?thesis ..
qed
text ‹
The general ‹⨅› (meet) and ‹⨆› (join) operations select
such infimum and supremum elements.
›
definition
Meet :: "'a::complete_lattice set ⇒ 'a" ("⨅_" [90] 90) where
"⨅A = (THE inf. is_Inf A inf)"
definition
Join :: "'a::complete_lattice set ⇒ 'a" ("⨆_" [90] 90) where
"⨆A = (THE sup. is_Sup A sup)"
text ‹
Due to unique existence of bounds, the complete lattice operations
may be exhibited as follows.
›
lemma Meet_equality [elim?]: "is_Inf A inf ⟹ ⨅A = inf"
proof (unfold Meet_def)
assume "is_Inf A inf"
then show "(THE inf. is_Inf A inf) = inf"
by (rule the_equality) (rule is_Inf_uniq [OF _ ‹is_Inf A inf›])
qed
lemma MeetI [intro?]:
"(⋀a. a ∈ A ⟹ inf ⊑ a) ⟹
(⋀b. ∀a ∈ A. b ⊑ a ⟹ b ⊑ inf) ⟹
⨅A = inf"
by (rule Meet_equality, rule is_InfI) blast+
lemma Join_equality [elim?]: "is_Sup A sup ⟹ ⨆A = sup"
proof (unfold Join_def)
assume "is_Sup A sup"
then show "(THE sup. is_Sup A sup) = sup"
by (rule the_equality) (rule is_Sup_uniq [OF _ ‹is_Sup A sup›])
qed
lemma JoinI [intro?]:
"(⋀a. a ∈ A ⟹ a ⊑ sup) ⟹
(⋀b. ∀a ∈ A. a ⊑ b ⟹ sup ⊑ b) ⟹
⨆A = sup"
by (rule Join_equality, rule is_SupI) blast+
text ‹
\medskip The ‹⨅› and ‹⨆› operations indeed determine
bounds on a complete lattice structure.
›
lemma is_Inf_Meet [intro?]: "is_Inf A (⨅A)"
proof (unfold Meet_def)
from ex_Inf obtain inf where "is_Inf A inf" ..
then show "is_Inf A (THE inf. is_Inf A inf)"
by (rule theI) (rule is_Inf_uniq [OF _ ‹is_Inf A inf›])
qed
lemma Meet_greatest [intro?]: "(⋀a. a ∈ A ⟹ x ⊑ a) ⟹ x ⊑ ⨅A"
by (rule is_Inf_greatest, rule is_Inf_Meet) blast
lemma Meet_lower [intro?]: "a ∈ A ⟹ ⨅A ⊑ a"
by (rule is_Inf_lower) (rule is_Inf_Meet)
lemma is_Sup_Join [intro?]: "is_Sup A (⨆A)"
proof (unfold Join_def)
from ex_Sup obtain sup where "is_Sup A sup" ..
then show "is_Sup A (THE sup. is_Sup A sup)"
by (rule theI) (rule is_Sup_uniq [OF _ ‹is_Sup A sup›])
qed
lemma Join_least [intro?]: "(⋀a. a ∈ A ⟹ a ⊑ x) ⟹ ⨆A ⊑ x"
by (rule is_Sup_least, rule is_Sup_Join) blast
lemma Join_lower [intro?]: "a ∈ A ⟹ a ⊑ ⨆A"
by (rule is_Sup_upper) (rule is_Sup_Join)
subsection ‹The Knaster-Tarski Theorem›
text ‹
The Knaster-Tarski Theorem (in its simplest formulation) states that
any monotone function on a complete lattice has a least fixed-point
(see \<^cite>‹‹pages 93--94› in "Davey-Priestley:1990"› for example). This
is a consequence of the basic boundary properties of the complete
lattice operations.
›
theorem Knaster_Tarski:
assumes mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y"
obtains a :: "'a::complete_lattice" where
"f a = a" and "⋀a'. f a' = a' ⟹ a ⊑ a'"
proof
let ?H = "{u. f u ⊑ u}"
let ?a = "⨅?H"
show "f ?a = ?a"
proof -
have ge: "f ?a ⊑ ?a"
proof
fix x assume x: "x ∈ ?H"
then have "?a ⊑ x" ..
then have "f ?a ⊑ f x" by (rule mono)
also from x have "... ⊑ x" ..
finally show "f ?a ⊑ x" .
qed
also have "?a ⊑ f ?a"
proof
from ge have "f (f ?a) ⊑ f ?a" by (rule mono)
then show "f ?a ∈ ?H" ..
qed
finally show ?thesis .
qed
fix a'
assume "f a' = a'"
then have "f a' ⊑ a'" by (simp only: leq_refl)
then have "a' ∈ ?H" ..
then show "?a ⊑ a'" ..
qed
theorem Knaster_Tarski_dual:
assumes mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y"
obtains a :: "'a::complete_lattice" where
"f a = a" and "⋀a'. f a' = a' ⟹ a' ⊑ a"
proof
let ?H = "{u. u ⊑ f u}"
let ?a = "⨆?H"
show "f ?a = ?a"
proof -
have le: "?a ⊑ f ?a"
proof
fix x assume x: "x ∈ ?H"
then have "x ⊑ f x" ..
also from x have "x ⊑ ?a" ..
then have "f x ⊑ f ?a" by (rule mono)
finally show "x ⊑ f ?a" .
qed
have "f ?a ⊑ ?a"
proof
from le have "f ?a ⊑ f (f ?a)" by (rule mono)
then show "f ?a ∈ ?H" ..
qed
from this and le show ?thesis by (rule leq_antisym)
qed
fix a'
assume "f a' = a'"
then have "a' ⊑ f a'" by (simp only: leq_refl)
then have "a' ∈ ?H" ..
then show "a' ⊑ ?a" ..
qed
subsection ‹Bottom and top elements›
text ‹
With general bounds available, complete lattices also have least and
greatest elements.
›
definition
bottom :: "'a::complete_lattice" ("⊥") where
"⊥ = ⨅UNIV"
definition
top :: "'a::complete_lattice" ("⊤") where
"⊤ = ⨆UNIV"
lemma bottom_least [intro?]: "⊥ ⊑ x"
proof (unfold bottom_def)
have "x ∈ UNIV" ..
then show "⨅UNIV ⊑ x" ..
qed
lemma bottomI [intro?]: "(⋀a. x ⊑ a) ⟹ ⊥ = x"
proof (unfold bottom_def)
assume "⋀a. x ⊑ a"
show "⨅UNIV = x"
proof
fix a show "x ⊑ a" by fact
next
fix b :: "'a::complete_lattice"
assume b: "∀a ∈ UNIV. b ⊑ a"
have "x ∈ UNIV" ..
with b show "b ⊑ x" ..
qed
qed
lemma top_greatest [intro?]: "x ⊑ ⊤"
proof (unfold top_def)
have "x ∈ UNIV" ..
then show "x ⊑ ⨆UNIV" ..
qed
lemma topI [intro?]: "(⋀a. a ⊑ x) ⟹ ⊤ = x"
proof (unfold top_def)
assume "⋀a. a ⊑ x"
show "⨆UNIV = x"
proof
fix a show "a ⊑ x" by fact
next
fix b :: "'a::complete_lattice"
assume b: "∀a ∈ UNIV. a ⊑ b"
have "x ∈ UNIV" ..
with b show "x ⊑ b" ..
qed
qed
subsection ‹Duality›
text ‹
The class of complete lattices is closed under formation of dual
structures.
›
instance dual :: (complete_lattice) complete_lattice
proof
fix A' :: "'a::complete_lattice dual set"
show "∃inf'. is_Inf A' inf'"
proof -
have "∃sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
then have "∃sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
then show ?thesis by (simp add: dual_ex [symmetric] image_comp)
qed
qed
text ‹
Apparently, the ‹⨅› and ‹⨆› operations are dual to each
other.
›
theorem dual_Meet [intro?]: "dual (⨅A) = ⨆(dual ` A)"
proof -
from is_Inf_Meet have "is_Sup (dual ` A) (dual (⨅A))" ..
then have "⨆(dual ` A) = dual (⨅A)" ..
then show ?thesis ..
qed
theorem dual_Join [intro?]: "dual (⨆A) = ⨅(dual ` A)"
proof -
from is_Sup_Join have "is_Inf (dual ` A) (dual (⨆A))" ..
then have "⨅(dual ` A) = dual (⨆A)" ..
then show ?thesis ..
qed
text ‹
Likewise are ‹⊥› and ‹⊤› duals of each other.
›
theorem dual_bottom [intro?]: "dual ⊥ = ⊤"
proof -
have "⊤ = dual ⊥"
proof
fix a' have "⊥ ⊑ undual a'" ..
then have "dual (undual a') ⊑ dual ⊥" ..
then show "a' ⊑ dual ⊥" by simp
qed
then show ?thesis ..
qed
theorem dual_top [intro?]: "dual ⊤ = ⊥"
proof -
have "⊥ = dual ⊤"
proof
fix a' have "undual a' ⊑ ⊤" ..
then have "dual ⊤ ⊑ dual (undual a')" ..
then show "dual ⊤ ⊑ a'" by simp
qed
then show ?thesis ..
qed
subsection ‹Complete lattices are lattices›
text ‹
Complete lattices (with general bounds available) are indeed plain
lattices as well. This holds due to the connection of general
versus binary bounds that has been formally established in
\S\ref{sec:gen-bin-bounds}.
›
lemma is_inf_binary: "is_inf x y (⨅{x, y})"
proof -
have "is_Inf {x, y} (⨅{x, y})" ..
then show ?thesis by (simp only: is_Inf_binary)
qed
lemma is_sup_binary: "is_sup x y (⨆{x, y})"
proof -
have "is_Sup {x, y} (⨆{x, y})" ..
then show ?thesis by (simp only: is_Sup_binary)
qed
instance complete_lattice ⊆ lattice
proof
fix x y :: "'a::complete_lattice"
from is_inf_binary show "∃inf. is_inf x y inf" ..
from is_sup_binary show "∃sup. is_sup x y sup" ..
qed
theorem meet_binary: "x ⊓ y = ⨅{x, y}"
by (rule meet_equality) (rule is_inf_binary)
theorem join_binary: "x ⊔ y = ⨆{x, y}"
by (rule join_equality) (rule is_sup_binary)
subsection ‹Complete lattices and set-theory operations›
text ‹
The complete lattice operations are (anti) monotone wrt.\ set
inclusion.
›
theorem Meet_subset_antimono: "A ⊆ B ⟹ ⨅B ⊑ ⨅A"
proof (rule Meet_greatest)
fix a assume "a ∈ A"
also assume "A ⊆ B"
finally have "a ∈ B" .
then show "⨅B ⊑ a" ..
qed
theorem Join_subset_mono: "A ⊆ B ⟹ ⨆A ⊑ ⨆B"
proof -
assume "A ⊆ B"
then have "dual ` A ⊆ dual ` B" by blast
then have "⨅(dual ` B) ⊑ ⨅(dual ` A)" by (rule Meet_subset_antimono)
then have "dual (⨆B) ⊑ dual (⨆A)" by (simp only: dual_Join)
then show ?thesis by (simp only: dual_leq)
qed
text ‹
Bounds over unions of sets may be obtained separately.
›
theorem Meet_Un: "⨅(A ∪ B) = ⨅A ⊓ ⨅B"
proof
fix a assume "a ∈ A ∪ B"
then show "⨅A ⊓ ⨅B ⊑ a"
proof
assume a: "a ∈ A"
have "⨅A ⊓ ⨅B ⊑ ⨅A" ..
also from a have "… ⊑ a" ..
finally show ?thesis .
next
assume a: "a ∈ B"
have "⨅A ⊓ ⨅B ⊑ ⨅B" ..
also from a have "… ⊑ a" ..
finally show ?thesis .
qed
next
fix b assume b: "∀a ∈ A ∪ B. b ⊑ a"
show "b ⊑ ⨅A ⊓ ⨅B"
proof
show "b ⊑ ⨅A"
proof
fix a assume "a ∈ A"
then have "a ∈ A ∪ B" ..
with b show "b ⊑ a" ..
qed
show "b ⊑ ⨅B"
proof
fix a assume "a ∈ B"
then have "a ∈ A ∪ B" ..
with b show "b ⊑ a" ..
qed
qed
qed
theorem Join_Un: "⨆(A ∪ B) = ⨆A ⊔ ⨆B"
proof -
have "dual (⨆(A ∪ B)) = ⨅(dual ` A ∪ dual ` B)"
by (simp only: dual_Join image_Un)
also have "… = ⨅(dual ` A) ⊓ ⨅(dual ` B)"
by (rule Meet_Un)
also have "… = dual (⨆A ⊔ ⨆B)"
by (simp only: dual_join dual_Join)
finally show ?thesis ..
qed
text ‹
Bounds over singleton sets are trivial.
›
theorem Meet_singleton: "⨅{x} = x"
proof
fix a assume "a ∈ {x}"
then have "a = x" by simp
then show "x ⊑ a" by (simp only: leq_refl)
next
fix b assume "∀a ∈ {x}. b ⊑ a"
then show "b ⊑ x" by simp
qed
theorem Join_singleton: "⨆{x} = x"
proof -
have "dual (⨆{x}) = ⨅{dual x}" by (simp add: dual_Join)
also have "… = dual x" by (rule Meet_singleton)
finally show ?thesis ..
qed
text ‹
Bounds over the empty and universal set correspond to each other.
›
theorem Meet_empty: "⨅{} = ⨆UNIV"
proof
fix a :: "'a::complete_lattice"
assume "a ∈ {}"
then have False by simp
then show "⨆UNIV ⊑ a" ..
next
fix b :: "'a::complete_lattice"
have "b ∈ UNIV" ..
then show "b ⊑ ⨆UNIV" ..
qed
theorem Join_empty: "⨆{} = ⨅UNIV"
proof -
have "dual (⨆{}) = ⨅{}" by (simp add: dual_Join)
also have "… = ⨆UNIV" by (rule Meet_empty)
also have "… = dual (⨅UNIV)" by (simp add: dual_Meet)
finally show ?thesis ..
qed
end