(* Title: HOL/Lattice/CompleteLattice.thy
Author: Markus Wenzel, TU Muenchen
*)
section \<open>Complete lattices\<close>
theory CompleteLattice imports Lattice begin
subsection \<open>Complete lattice operations\<close>
text \<open>
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}).
\<close>
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 \<open>
The general \<open>\<Sqinter>\<close> (meet) and \<open>\<Squnion>\<close> (join) operations select
such infimum and supremum elements.
\<close>
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 \<open>
Due to unique existence of bounds, the complete lattice operations
may be exhibited as follows.
\<close>
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 _ \<open>is_Inf A inf\<close>])
qed
lemma MeetI [intro?]:
"(\a. a \ A \ inf \ a) \
(\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>
\<Sqinter>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 _ \<open>is_Sup A sup\<close>])
qed
lemma JoinI [intro?]:
"(\a. a \ A \ a \ sup) \
(\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>
\<Squnion>A = sup"
by (rule Join_equality, rule is_SupI) blast+
text \<open>
\medskip The \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations indeed determine
bounds on a complete lattice structure.
\<close>
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 _ \<open>is_Inf A inf\<close>])
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 _ \<open>is_Sup A sup\<close>])
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 \<open>The Knaster-Tarski Theorem\<close>
text \<open>
The Knaster-Tarski Theorem (in its simplest formulation) states that
any monotone function on a complete lattice has a least fixed-point
(see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example). This
is a consequence of the basic boundary properties of the complete
lattice operations.
\<close>
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 \<open>Bottom and top elements\<close>
text \<open>
With general bounds available, complete lattices also have least and
greatest elements.
\<close>
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 \<open>Duality\<close>
text \<open>
The class of complete lattices is closed under formation of dual
structures.
\<close>
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 \<open>
Apparently, the \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations are dual to each
other.
\<close>
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 \<open>
Likewise are \<open>\<bottom>\<close> and \<open>\<top>\<close> duals of each other.
\<close>
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' \<sqsubseteq> \<top>" ..
then have "dual \ \ dual (undual a')" ..
then show "dual \ \ a'" by simp
qed
then show ?thesis ..
qed
subsection \<open>Complete lattices are lattices\<close>
text \<open>
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}.
\<close>
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 \<subseteq> 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 \<open>Complete lattices and set-theory operations\<close>
text \<open>
The complete lattice operations are (anti) monotone wrt.\ set
inclusion.
\<close>
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 \<open>
Bounds over unions of sets may be obtained separately.
\<close>
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 \<open>
Bounds over singleton sets are trivial.
\<close>
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 \<open>
Bounds over the empty and universal set correspond to each other.
\<close>
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
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
