--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/CompleteLattice.thy Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,409 @@
+(* Title: HOL/Lattice/CompleteLattice.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+header {* Complete lattices *}
+
+theory CompleteLattice = Lattice:
+
+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}).
+*}
+
+axclass complete_lattice < partial_order
+ ex_Inf: "\<exists>inf. is_Inf A inf"
+
+theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
+proof -
+ from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
+ hence "is_Sup A sup" by (rule Inf_Sup)
+ thus ?thesis ..
+qed
+
+text {*
+ The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
+ such infimum and supremum elements.
+*}
+
+consts
+ Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
+ Join :: "'a::complete_lattice set \<Rightarrow> 'a"
+syntax (symbols)
+ Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
+ Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
+defs
+ Meet_def: "\<Sqinter>A \<equiv> SOME inf. is_Inf A inf"
+ Join_def: "\<Squnion>A \<equiv> SOME 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 \<Longrightarrow> \<Sqinter>A = inf"
+proof (unfold Meet_def)
+ assume "is_Inf A inf"
+ thus "(SOME inf. is_Inf A inf) = inf"
+ by (rule some_equality) (rule is_Inf_uniq)
+qed
+
+lemma MeetI [intro?]:
+ "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow>
+ (\<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 \<Longrightarrow> \<Squnion>A = sup"
+proof (unfold Join_def)
+ assume "is_Sup A sup"
+ thus "(SOME sup. is_Sup A sup) = sup"
+ by (rule some_equality) (rule is_Sup_uniq)
+qed
+
+lemma JoinI [intro?]:
+ "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow>
+ (\<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 {*
+ \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
+ bounds on a complete lattice structure.
+*}
+
+lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
+proof (unfold Meet_def)
+ from ex_Inf show "is_Inf A (SOME inf. is_Inf A inf)"
+ by (rule ex_someI)
+qed
+
+lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
+ by (rule is_Inf_greatest, rule is_Inf_Meet) blast
+
+lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a"
+ by (rule is_Inf_lower) (rule is_Inf_Meet)
+
+
+lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
+proof (unfold Join_def)
+ from ex_Sup show "is_Sup A (SOME sup. is_Sup A sup)"
+ by (rule ex_someI)
+qed
+
+lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
+ by (rule is_Sup_least, rule is_Sup_Join) blast
+lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>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]{Davey-Priestley:1990} for example). This
+ is a consequence of the basic boundary properties of the complete
+ lattice operations.
+*}
+
+theorem Knaster_Tarski:
+ "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"
+proof
+ assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+ let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
+ have ge: "f ?a \<sqsubseteq> ?a"
+ proof
+ fix x assume x: "x \<in> ?H"
+ hence "?a \<sqsubseteq> x" ..
+ hence "f ?a \<sqsubseteq> f x" by (rule mono)
+ also from x have "... \<sqsubseteq> x" ..
+ finally show "f ?a \<sqsubseteq> x" .
+ qed
+ also have "?a \<sqsubseteq> f ?a"
+ proof
+ from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
+ thus "f ?a : ?H" ..
+ qed
+ finally show "f ?a = ?a" .
+qed
+
+
+subsection {* Bottom and top elements *}
+
+text {*
+ With general bounds available, complete lattices also have least and
+ greatest elements.
+*}
+
+constdefs
+ bottom :: "'a::complete_lattice" ("\<bottom>")
+ "\<bottom> \<equiv> \<Sqinter>UNIV"
+ top :: "'a::complete_lattice" ("\<top>")
+ "\<top> \<equiv> \<Squnion>UNIV"
+
+lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
+proof (unfold bottom_def)
+ have "x \<in> UNIV" ..
+ thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
+qed
+
+lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
+proof (unfold bottom_def)
+ assume "\<And>a. x \<sqsubseteq> a"
+ show "\<Sqinter>UNIV = x"
+ proof
+ fix a show "x \<sqsubseteq> a" .
+ next
+ fix b :: "'a::complete_lattice"
+ assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
+ have "x \<in> UNIV" ..
+ with b show "b \<sqsubseteq> x" ..
+ qed
+qed
+
+lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
+proof (unfold top_def)
+ have "x \<in> UNIV" ..
+ thus "x \<sqsubseteq> \<Squnion>UNIV" ..
+qed
+
+lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
+proof (unfold top_def)
+ assume "\<And>a. a \<sqsubseteq> x"
+ show "\<Squnion>UNIV = x"
+ proof
+ fix a show "a \<sqsubseteq> x" .
+ next
+ fix b :: "'a::complete_lattice"
+ assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
+ have "x \<in> UNIV" ..
+ with b show "x \<sqsubseteq> 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 intro_classes
+ fix A' :: "'a::complete_lattice dual set"
+ show "\<exists>inf'. is_Inf A' inf'"
+ proof -
+ have "\<exists>sup. is_Sup (undual `` A') sup" by (rule ex_Sup)
+ hence "\<exists>sup. is_Inf (dual `` undual `` A') (dual sup)" by (simp only: dual_Inf)
+ thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
+ qed
+qed
+
+text {*
+ Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
+ other.
+*}
+
+theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual `` A)"
+proof -
+ from is_Inf_Meet have "is_Sup (dual `` A) (dual (\<Sqinter>A))" ..
+ hence "\<Squnion>(dual `` A) = dual (\<Sqinter>A)" ..
+ thus ?thesis ..
+qed
+
+theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual `` A)"
+proof -
+ from is_Sup_Join have "is_Inf (dual `` A) (dual (\<Squnion>A))" ..
+ hence "\<Sqinter>(dual `` A) = dual (\<Squnion>A)" ..
+ thus ?thesis ..
+qed
+
+text {*
+ Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
+*}
+
+theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
+proof -
+ have "\<top> = dual \<bottom>"
+ proof
+ fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
+ hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
+ thus "a' \<sqsubseteq> dual \<bottom>" by simp
+ qed
+ thus ?thesis ..
+qed
+
+theorem dual_top [intro?]: "dual \<top> = \<bottom>"
+proof -
+ have "\<bottom> = dual \<top>"
+ proof
+ fix a' have "undual a' \<sqsubseteq> \<top>" ..
+ hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
+ thus "dual \<top> \<sqsubseteq> a'" by simp
+ qed
+ thus ?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 (\<Sqinter>{x, y})"
+proof -
+ have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
+ thus ?thesis by (simp only: is_Inf_binary)
+qed
+
+lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
+proof -
+ have "is_Sup {x, y} (\<Squnion>{x, y})" ..
+ thus ?thesis by (simp only: is_Sup_binary)
+qed
+
+instance complete_lattice < lattice
+proof intro_classes
+ fix x y :: "'a::complete_lattice"
+ from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
+ from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
+qed
+
+theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"
+ by (rule meet_equality) (rule is_inf_binary)
+
+theorem join_binary: "x \<squnion> y = \<Squnion>{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 \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
+proof (rule Meet_greatest)
+ fix a assume "a \<in> A"
+ also assume "A \<subseteq> B"
+ finally have "a \<in> B" .
+ thus "\<Sqinter>B \<sqsubseteq> a" ..
+qed
+
+theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
+proof -
+ assume "A \<subseteq> B"
+ hence "dual `` A \<subseteq> dual `` B" by blast
+ hence "\<Sqinter>(dual `` B) \<sqsubseteq> \<Sqinter>(dual `` A)" by (rule Meet_subset_antimono)
+ hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
+ thus ?thesis by (simp only: dual_leq)
+qed
+
+text {*
+ Bounds over unions of sets may be obtained separately.
+*}
+
+theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
+proof
+ fix a assume "a \<in> A \<union> B"
+ thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
+ proof
+ assume a: "a \<in> A"
+ have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
+ also from a have "\<dots> \<sqsubseteq> a" ..
+ finally show ?thesis .
+ next
+ assume a: "a \<in> B"
+ have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
+ also from a have "\<dots> \<sqsubseteq> a" ..
+ finally show ?thesis .
+ qed
+next
+ fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"
+ show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
+ proof
+ show "b \<sqsubseteq> \<Sqinter>A"
+ proof
+ fix a assume "a \<in> A"
+ hence "a \<in> A \<union> B" ..
+ with b show "b \<sqsubseteq> a" ..
+ qed
+ show "b \<sqsubseteq> \<Sqinter>B"
+ proof
+ fix a assume "a \<in> B"
+ hence "a \<in> A \<union> B" ..
+ with b show "b \<sqsubseteq> a" ..
+ qed
+ qed
+qed
+
+theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
+proof -
+ have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual `` A \<union> dual `` B)"
+ by (simp only: dual_Join image_Un)
+ also have "\<dots> = \<Sqinter>(dual `` A) \<sqinter> \<Sqinter>(dual `` B)"
+ by (rule Meet_Un)
+ also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
+ by (simp only: dual_join dual_Join)
+ finally show ?thesis ..
+qed
+
+text {*
+ Bounds over singleton sets are trivial.
+*}
+
+theorem Meet_singleton: "\<Sqinter>{x} = x"
+proof
+ fix a assume "a \<in> {x}"
+ hence "a = x" by simp
+ thus "x \<sqsubseteq> a" by (simp only: leq_refl)
+next
+ fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
+ thus "b \<sqsubseteq> x" by simp
+qed
+
+theorem Join_singleton: "\<Squnion>{x} = x"
+proof -
+ have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)
+ also have "\<dots> = 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: "\<Sqinter>{} = \<Squnion>UNIV"
+proof
+ fix a :: "'a::complete_lattice"
+ assume "a \<in> {}"
+ hence False by simp
+ thus "\<Squnion>UNIV \<sqsubseteq> a" ..
+next
+ fix b :: "'a::complete_lattice"
+ have "b \<in> UNIV" ..
+ thus "b \<sqsubseteq> \<Squnion>UNIV" ..
+qed
+
+theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
+proof -
+ have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
+ also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)
+ also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
+ finally show ?thesis ..
+qed
+
+end