--- a/NEWS Thu Oct 05 14:04:56 2000 +0200
+++ b/NEWS Fri Oct 06 01:04:56 2000 +0200
@@ -243,10 +243,17 @@
* HOL/Algebra: new theory of rings and univariate polynomials, by
Clemens Ballarin;
-* HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese
+* HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese
Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M
Rasmussen;
+* HOL/Lattice: fundamental concepts of lattice theory and order
+structures, including duals, properties of bounds versus algebraic
+laws, lattice operations versus set-theoretic ones, the Knaster-Tarski
+Theorem for complete lattices etc.; may also serve as a demonstration
+for abstract algebraic reasoning using axiomatic type classes, and
+mathematics-style proof in Isabelle/Isar; by Markus Wenzel;
+
* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
von Oheimb;
--- a/src/HOL/IsaMakefile Thu Oct 05 14:04:56 2000 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 06 01:04:56 2000 +0200
@@ -9,13 +9,38 @@
default: HOL
images: HOL HOL-Real TLA
-test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-AxClasses HOL-ex HOL-Subst HOL-IMP \
- HOL-IMPP HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth \
- HOL-UNITY HOL-Modelcheck HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV \
- HOL-MicroJava HOL-IOA HOL-Real-ex HOL-Real-HahnBanach \
- TLA-Inc TLA-Buffer TLA-Memory
-
-all: images test
+#Note: keep targets sorted!
+test: \
+ HOL-Algebra \
+ HOL-Auth \
+ HOL-AxClasses \
+ HOL-BCV \
+ HOL-Real-HahnBanach \
+ HOL-Real-ex \
+ HOL-Hoare \
+ HOL-IMP \
+ HOL-IMPP \
+ HOL-IOA \
+ HOL-Induct \
+ HOL-Isar_examples \
+ HOL-Lambda \
+ HOL-Lattice \
+ HOL-Lex \
+ HOL-MicroJava \
+ HOL-MiniML \
+ HOL-Modelcheck \
+ HOL-NumberTheory \
+ HOL-Prolog \
+ HOL-Subst \
+ TLA-Buffer \
+ TLA-Inc \
+ TLA-Memory \
+ HOL-UNITY \
+ HOL-W0 \
+ HOL-ex
+ # ^ this is the sort position
+
+all: test images
## global settings
@@ -406,6 +431,16 @@
@$(ISATOOL) usedir $(OUT)/HOL AxClasses
+## HOL-Lattice
+
+HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
+
+$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
+ Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
+ Lattice/ROOT.ML Lattice/document/root.tex
+ @$(ISATOOL) usedir $(OUT)/HOL Lattice
+
+
## HOL-ex
HOL-ex: HOL $(LOG)/HOL-ex.gz
@@ -502,6 +537,6 @@
$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
- $(LOG)/HOL-Real-ex.gz \
+ $(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/Bounds.thy Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,325 @@
+(* Title: HOL/Lattice/Bounds.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+header {* Bounds *}
+
+theory Bounds = Orders:
+
+subsection {* Infimum and supremum *}
+
+text {*
+ Given a partial order, we define infimum (greatest lower bound) and
+ supremum (least upper bound) wrt.\ @{text \<sqsubseteq>} for two and for any
+ number of elements.
+*}
+
+constdefs
+ is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ "is_inf x y inf \<equiv> inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf)"
+
+ is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ "is_sup x y sup \<equiv> x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z)"
+
+ is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
+ "is_Inf A inf \<equiv> (\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf)"
+
+ is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
+ "is_Sup A sup \<equiv> (\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z)"
+
+text {*
+ These definitions entail the following basic properties of boundary
+ elements.
+*}
+
+lemma is_infI [intro?]: "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow>
+ (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_inf x y inf"
+ by (unfold is_inf_def) blast
+
+lemma is_inf_greatest [elim?]:
+ "is_inf x y inf \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf"
+ by (unfold is_inf_def) blast
+
+lemma is_inf_lower [elim?]:
+ "is_inf x y inf \<Longrightarrow> (inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
+ by (unfold is_inf_def) blast
+
+
+lemma is_supI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
+ (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_sup x y sup"
+ by (unfold is_sup_def) blast
+
+lemma is_sup_least [elim?]:
+ "is_sup x y sup \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z"
+ by (unfold is_sup_def) blast
+
+lemma is_sup_upper [elim?]:
+ "is_sup x y sup \<Longrightarrow> (x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow> C) \<Longrightarrow> C"
+ by (unfold is_sup_def) blast
+
+
+lemma is_InfI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> inf \<sqsubseteq> x) \<Longrightarrow>
+ (\<And>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_Inf A inf"
+ by (unfold is_Inf_def) blast
+
+lemma is_Inf_greatest [elim?]:
+ "is_Inf A inf \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf"
+ by (unfold is_Inf_def) blast
+
+lemma is_Inf_lower [dest?]:
+ "is_Inf A inf \<Longrightarrow> x \<in> A \<Longrightarrow> inf \<sqsubseteq> x"
+ by (unfold is_Inf_def) blast
+
+
+lemma is_SupI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> sup) \<Longrightarrow>
+ (\<And>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_Sup A sup"
+ by (unfold is_Sup_def) blast
+
+lemma is_Sup_least [elim?]:
+ "is_Sup A sup \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z"
+ by (unfold is_Sup_def) blast
+
+lemma is_Sup_upper [dest?]:
+ "is_Sup A sup \<Longrightarrow> x \<in> A \<Longrightarrow> x \<sqsubseteq> sup"
+ by (unfold is_Sup_def) blast
+
+
+subsection {* Duality *}
+
+text {*
+ Infimum and supremum are dual to each other.
+*}
+
+theorem dual_inf [iff?]:
+ "is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"
+ by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
+
+theorem dual_sup [iff?]:
+ "is_sup (dual x) (dual y) (dual inf) = is_inf x y inf"
+ by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
+
+theorem dual_Inf [iff?]:
+ "is_Inf (dual `` A) (dual sup) = is_Sup A sup"
+ by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
+
+theorem dual_Sup [iff?]:
+ "is_Sup (dual `` A) (dual inf) = is_Inf A inf"
+ by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
+
+
+subsection {* Uniqueness *}
+
+text {*
+ Infima and suprema on partial orders are unique; this is mainly due
+ to anti-symmetry of the underlying relation.
+*}
+
+theorem is_inf_uniq: "is_inf x y inf \<Longrightarrow> is_inf x y inf' \<Longrightarrow> inf = inf'"
+proof -
+ assume inf: "is_inf x y inf"
+ assume inf': "is_inf x y inf'"
+ show ?thesis
+ proof (rule leq_antisym)
+ from inf' show "inf \<sqsubseteq> inf'"
+ proof (rule is_inf_greatest)
+ from inf show "inf \<sqsubseteq> x" ..
+ from inf show "inf \<sqsubseteq> y" ..
+ qed
+ from inf show "inf' \<sqsubseteq> inf"
+ proof (rule is_inf_greatest)
+ from inf' show "inf' \<sqsubseteq> x" ..
+ from inf' show "inf' \<sqsubseteq> y" ..
+ qed
+ qed
+qed
+
+theorem is_sup_uniq: "is_sup x y sup \<Longrightarrow> is_sup x y sup' \<Longrightarrow> sup = sup'"
+proof -
+ assume sup: "is_sup x y sup" and sup': "is_sup x y sup'"
+ have "dual sup = dual sup'"
+ proof (rule is_inf_uniq)
+ from sup show "is_inf (dual x) (dual y) (dual sup)" ..
+ from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
+ qed
+ thus "sup = sup'" ..
+qed
+
+theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
+proof -
+ assume inf: "is_Inf A inf"
+ assume inf': "is_Inf A inf'"
+ show ?thesis
+ proof (rule leq_antisym)
+ from inf' show "inf \<sqsubseteq> inf'"
+ proof (rule is_Inf_greatest)
+ fix x assume "x \<in> A"
+ from inf show "inf \<sqsubseteq> x" ..
+ qed
+ from inf show "inf' \<sqsubseteq> inf"
+ proof (rule is_Inf_greatest)
+ fix x assume "x \<in> A"
+ from inf' show "inf' \<sqsubseteq> x" ..
+ qed
+ qed
+qed
+
+theorem is_Sup_uniq: "is_Sup A sup \<Longrightarrow> is_Sup A sup' \<Longrightarrow> sup = sup'"
+proof -
+ assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"
+ have "dual sup = dual sup'"
+ proof (rule is_Inf_uniq)
+ from sup show "is_Inf (dual `` A) (dual sup)" ..
+ from sup' show "is_Inf (dual `` A) (dual sup')" ..
+ qed
+ thus "sup = sup'" ..
+qed
+
+
+subsection {* Related elements *}
+
+text {*
+ The binary bound of related elements is either one of the argument.
+*}
+
+theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
+proof -
+ assume "x \<sqsubseteq> y"
+ show ?thesis
+ proof
+ show "x \<sqsubseteq> x" ..
+ show "x \<sqsubseteq> y" .
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
+ qed
+qed
+
+theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
+proof -
+ assume "x \<sqsubseteq> y"
+ show ?thesis
+ proof
+ show "x \<sqsubseteq> y" .
+ show "y \<sqsubseteq> y" ..
+ fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
+ show "y \<sqsubseteq> z" .
+ qed
+qed
+
+
+subsection {* General versus binary bounds \label{sec:gen-bin-bounds} *}
+
+text {*
+ General bounds of two-element sets coincide with binary bounds.
+*}
+
+theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"
+proof -
+ let ?A = "{x, y}"
+ show ?thesis
+ proof
+ assume is_Inf: "is_Inf ?A inf"
+ show "is_inf x y inf"
+ proof
+ have "x \<in> ?A" by simp
+ with is_Inf show "inf \<sqsubseteq> x" ..
+ have "y \<in> ?A" by simp
+ with is_Inf show "inf \<sqsubseteq> y" ..
+ fix z assume zx: "z \<sqsubseteq> x" and zy: "z \<sqsubseteq> y"
+ from is_Inf show "z \<sqsubseteq> inf"
+ proof (rule is_Inf_greatest)
+ fix a assume "a \<in> ?A"
+ hence "a = x \<or> a = y" by blast
+ thus "z \<sqsubseteq> a"
+ proof
+ assume "a = x"
+ with zx show ?thesis by simp
+ next
+ assume "a = y"
+ with zy show ?thesis by simp
+ qed
+ qed
+ qed
+ next
+ assume is_inf: "is_inf x y inf"
+ show "is_Inf {x, y} inf"
+ proof
+ fix a assume "a \<in> ?A"
+ hence "a = x \<or> a = y" by blast
+ thus "inf \<sqsubseteq> a"
+ proof
+ assume "a = x"
+ also from is_inf have "inf \<sqsubseteq> x" ..
+ finally show ?thesis .
+ next
+ assume "a = y"
+ also from is_inf have "inf \<sqsubseteq> y" ..
+ finally show ?thesis .
+ qed
+ next
+ fix z assume z: "\<forall>a \<in> ?A. z \<sqsubseteq> a"
+ from is_inf show "z \<sqsubseteq> inf"
+ proof (rule is_inf_greatest)
+ from z show "z \<sqsubseteq> x" by blast
+ from z show "z \<sqsubseteq> y" by blast
+ qed
+ qed
+ qed
+qed
+
+theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"
+proof -
+ have "is_Sup {x, y} sup = is_Inf (dual `` {x, y}) (dual sup)"
+ by (simp only: dual_Inf)
+ also have "dual `` {x, y} = {dual x, dual y}"
+ by simp
+ also have "is_Inf \<dots> (dual sup) = is_inf (dual x) (dual y) (dual sup)"
+ by (rule is_Inf_binary)
+ also have "\<dots> = is_sup x y sup"
+ by (simp only: dual_inf)
+ finally show ?thesis .
+qed
+
+
+subsection {* Connecting general bounds \label{sec:connect-bounds} *}
+
+text {*
+ Either kind of general bounds is sufficient to express the other.
+ The least upper bound (supremum) is the same as the the greatest
+ lower bound of the set of all upper bounds; the dual statements
+ holds as well; the dual statement holds as well.
+*}
+
+theorem Inf_Sup: "is_Inf {b. \<forall>a \<in> A. a \<sqsubseteq> b} sup \<Longrightarrow> is_Sup A sup"
+proof -
+ let ?B = "{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
+ assume is_Inf: "is_Inf ?B sup"
+ show "is_Sup A sup"
+ proof
+ fix x assume x: "x \<in> A"
+ from is_Inf show "x \<sqsubseteq> sup"
+ proof (rule is_Inf_greatest)
+ fix y assume "y \<in> ?B"
+ hence "\<forall>a \<in> A. a \<sqsubseteq> y" ..
+ from this x show "x \<sqsubseteq> y" ..
+ qed
+ next
+ fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
+ hence "z \<in> ?B" ..
+ with is_Inf show "sup \<sqsubseteq> z" ..
+ qed
+qed
+
+theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
+proof -
+ assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
+ hence "is_Inf (dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
+ by (simp only: dual_Inf dual_leq)
+ also have "dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual `` A. a' \<sqsubseteq> b'}"
+ by (auto iff: dual_ball dual_Collect) (* FIXME !? *)
+ finally have "is_Inf \<dots> (dual inf)" .
+ hence "is_Sup (dual `` A) (dual inf)"
+ by (rule Inf_Sup)
+ thus ?thesis ..
+qed
+
+end
--- /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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/Lattice.thy Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,609 @@
+(* Title: HOL/Lattice/Lattice.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+header {* Lattices *}
+
+theory Lattice = Bounds:
+
+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).
+*}
+
+axclass lattice < partial_order
+ ex_inf: "\<exists>inf. is_inf x y inf"
+ ex_sup: "\<exists>sup. is_sup x y sup"
+
+text {*
+ The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
+ infimum and supremum elements.
+*}
+
+consts
+ meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70)
+ join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65)
+syntax (symbols)
+ meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
+ join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+defs
+ meet_def: "x && y \<equiv> SOME inf. is_inf x y inf"
+ join_def: "x || y \<equiv> SOME 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 \<Longrightarrow> x \<sqinter> y = inf"
+proof (unfold meet_def)
+ assume "is_inf x y inf"
+ thus "(SOME inf. is_inf x y inf) = inf"
+ by (rule some_equality) (rule is_inf_uniq)
+qed
+
+lemma meetI [intro?]:
+ "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> x \<sqinter> y = inf"
+ by (rule meet_equality, rule is_infI) blast+
+
+lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
+proof (unfold join_def)
+ assume "is_sup x y sup"
+ thus "(SOME sup. is_sup x y sup) = sup"
+ by (rule some_equality) (rule is_sup_uniq)
+qed
+
+lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
+ (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = sup"
+ by (rule join_equality, rule is_supI) blast+
+
+
+text {*
+ \medskip The @{text \<sqinter>} and @{text \<squnion>} operations indeed determine
+ bounds on a lattice structure.
+*}
+
+lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
+proof (unfold meet_def)
+ from ex_inf show "is_inf x y (SOME inf. is_inf x y inf)"
+ by (rule ex_someI)
+qed
+
+lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
+ by (rule is_inf_greatest) (rule is_inf_meet)
+
+lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"
+ by (rule is_inf_lower) (rule is_inf_meet)
+
+lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"
+ by (rule is_inf_lower) (rule is_inf_meet)
+
+
+lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
+proof (unfold join_def)
+ from ex_sup show "is_sup x y (SOME sup. is_sup x y sup)"
+ by (rule ex_someI)
+qed
+
+lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
+ by (rule is_sup_least) (rule is_sup_join)
+
+lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"
+ by (rule is_sup_upper) (rule is_sup_join)
+
+lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> 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 intro_classes
+ fix x' y' :: "'a::lattice dual"
+ show "\<exists>inf'. is_inf x' y' inf'"
+ proof -
+ have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
+ hence "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
+ by (simp only: dual_inf)
+ thus ?thesis by (simp add: dual_ex [symmetric])
+ qed
+ show "\<exists>sup'. is_sup x' y' sup'"
+ proof -
+ have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
+ hence "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
+ by (simp only: dual_sup)
+ thus ?thesis by (simp add: dual_ex [symmetric])
+ qed
+qed
+
+text {*
+ Apparently, the @{text \<sqinter>} and @{text \<squnion>} operations are dual to each
+ other.
+*}
+
+theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
+proof -
+ from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
+ hence "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
+ thus ?thesis ..
+qed
+
+theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
+proof -
+ from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
+ hence "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
+ thus ?thesis ..
+qed
+
+
+subsection {* Algebraic properties \label{sec:lattice-algebra} *}
+
+text {*
+ The @{text \<sqinter>} and @{text \<squnion>} operations have to following
+ characteristic algebraic properties: associative (A), commutative
+ (C), and absorptive (AB).
+*}
+
+theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+proof
+ show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
+ proof
+ show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
+ show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
+ proof -
+ have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
+ also have "\<dots> \<sqsubseteq> y" ..
+ finally show ?thesis .
+ qed
+ qed
+ show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
+ proof -
+ have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
+ also have "\<dots> \<sqsubseteq> z" ..
+ finally show ?thesis .
+ qed
+ fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
+ show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
+ proof
+ show "w \<sqsubseteq> x"
+ proof -
+ have "w \<sqsubseteq> x \<sqinter> y" .
+ also have "\<dots> \<sqsubseteq> x" ..
+ finally show ?thesis .
+ qed
+ show "w \<sqsubseteq> y \<sqinter> z"
+ proof
+ show "w \<sqsubseteq> y"
+ proof -
+ have "w \<sqsubseteq> x \<sqinter> y" .
+ also have "\<dots> \<sqsubseteq> y" ..
+ finally show ?thesis .
+ qed
+ show "w \<sqsubseteq> z" .
+ qed
+ qed
+qed
+
+theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+proof -
+ have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"
+ by (simp only: dual_join)
+ also have "\<dots> = dual x \<sqinter> (dual y \<sqinter> dual z)"
+ by (rule meet_assoc)
+ also have "\<dots> = dual (x \<squnion> (y \<squnion> z))"
+ by (simp only: dual_join)
+ finally show ?thesis ..
+qed
+
+theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
+proof
+ show "y \<sqinter> x \<sqsubseteq> x" ..
+ show "y \<sqinter> x \<sqsubseteq> y" ..
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
+ show "z \<sqsubseteq> y \<sqinter> x" ..
+qed
+
+theorem join_commute: "x \<squnion> y = y \<squnion> x"
+proof -
+ have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..
+ also have "\<dots> = dual y \<sqinter> dual x"
+ by (rule meet_commute)
+ also have "\<dots> = dual (y \<squnion> x)"
+ by (simp only: dual_join)
+ finally show ?thesis ..
+qed
+
+theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
+proof
+ show "x \<sqsubseteq> x" ..
+ show "x \<sqsubseteq> x \<squnion> y" ..
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
+ show "z \<sqsubseteq> x" .
+qed
+
+theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
+proof -
+ have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
+ by (rule meet_join_absorb)
+ hence "dual (x \<squnion> (x \<sqinter> y)) = dual x"
+ by (simp only: dual_meet dual_join)
+ thus ?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 \<sqinter> x = x"
+proof -
+ have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
+ also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
+ finally show ?thesis .
+qed
+
+theorem join_idem: "x \<squnion> x = x"
+proof -
+ have "dual x \<sqinter> dual x = dual x"
+ by (rule meet_idem)
+ hence "dual (x \<squnion> x) = dual x"
+ by (simp only: dual_join)
+ thus ?thesis ..
+qed
+
+text {*
+ Meet and join are trivial for related elements.
+*}
+
+theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+proof
+ assume "x \<sqsubseteq> y"
+ show "x \<sqsubseteq> x" ..
+ show "x \<sqsubseteq> y" .
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
+qed
+
+theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+proof -
+ assume "x \<sqsubseteq> y" hence "dual y \<sqsubseteq> dual x" ..
+ hence "dual y \<sqinter> dual x = dual y" by (rule meet_related)
+ also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
+ also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
+ finally show ?thesis ..
+qed
+
+
+subsection {* Order versus algebraic structure *}
+
+text {*
+ The @{text \<sqinter>} and @{text \<squnion>} operations are connected with the
+ underlying @{text \<sqsubseteq>} relation in a canonical manner.
+*}
+
+theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
+proof
+ assume "x \<sqsubseteq> y"
+ hence "is_inf x y x" ..
+ thus "x \<sqinter> y = x" ..
+next
+ have "x \<sqinter> y \<sqsubseteq> y" ..
+ also assume "x \<sqinter> y = x"
+ finally show "x \<sqsubseteq> y" .
+qed
+
+theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
+proof
+ assume "x \<sqsubseteq> y"
+ hence "is_sup x y y" ..
+ thus "x \<squnion> y = y" ..
+next
+ have "x \<sqsubseteq> x \<squnion> y" ..
+ also assume "x \<squnion> y = y"
+ finally show "x \<sqsubseteq> 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 \<sqinter>} and @{text \<squnion>}
+ such that (A), (C), and (AB) hold (cf.\
+ \S\ref{sec:lattice-algebra}). This structure represents a lattice,
+ if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}
+ (alternatively as @{term "x \<squnion> y = y"}). Furthermore, infimum and
+ supremum with respect to this ordering coincide with the original
+ @{text \<sqinter>} and @{text \<squnion>} operations.
+*}
+
+
+subsection {* Example instances *}
+
+subsubsection {* Linear orders *}
+
+text {*
+ Linear orders with @{term minimum} and @{term minimum} operations
+ are a (degenerate) example of lattice structures.
+*}
+
+constdefs
+ minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
+ "minimum x y \<equiv> (if x \<sqsubseteq> y then x else y)"
+ maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
+ "maximum x y \<equiv> (if x \<sqsubseteq> 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 \<sqsubseteq> x" by (auto simp add: minimum_def)
+ from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
+ with leq_linear show "z \<sqsubseteq> ?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 \<sqsubseteq> ?max" by (auto simp add: maximum_def)
+ from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)
+ fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
+ with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
+qed
+
+instance linear_order < lattice
+proof intro_classes
+ fix x y :: "'a::linear_order"
+ from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
+ from is_sup_maximum show "\<exists>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 \<sqinter> y = minimum x y"
+ by (rule meet_equality) (rule is_inf_minimum)
+
+theorem meet_maximum: "x \<squnion> 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.\
+ also \S\ref{sec:prod-order}).
+*}
+
+lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
+proof
+ show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"
+ proof -
+ have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..
+ moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..
+ ultimately show ?thesis by (simp add: leq_prod_def)
+ qed
+ show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"
+ proof -
+ have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..
+ moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..
+ ultimately show ?thesis by (simp add: leq_prod_def)
+ qed
+ fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"
+ show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
+ proof -
+ have "fst r \<sqsubseteq> fst p \<sqinter> fst q"
+ proof
+ from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)
+ from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)
+ qed
+ moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"
+ proof
+ from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)
+ from rq show "snd r \<sqsubseteq> 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 \<squnion> fst q, snd p \<squnion> snd q)" (* FIXME dualize!? *)
+proof
+ show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
+ proof -
+ have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..
+ moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..
+ ultimately show ?thesis by (simp add: leq_prod_def)
+ qed
+ show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
+ proof -
+ have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..
+ moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..
+ ultimately show ?thesis by (simp add: leq_prod_def)
+ qed
+ fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"
+ show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"
+ proof -
+ have "fst p \<squnion> fst q \<sqsubseteq> fst r"
+ proof
+ from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)
+ from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)
+ qed
+ moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"
+ proof
+ from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)
+ from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)
+ qed
+ ultimately show ?thesis by (simp add: leq_prod_def)
+ qed
+qed
+
+instance * :: (lattice, lattice) lattice
+proof intro_classes
+ fix p q :: "'a::lattice \<times> 'b::lattice"
+ from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
+ from is_sup_prod show "\<exists>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 \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
+ by (rule meet_equality) (rule is_inf_prod)
+
+theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> 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.\ also \S\ref{sec:fun-order}).
+*}
+
+lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"
+proof
+ show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> f"
+ proof
+ fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..
+ qed
+ show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> g"
+ proof
+ fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..
+ qed
+ fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"
+ show "h \<sqsubseteq> (\<lambda>x. f x \<sqinter> g x)"
+ proof
+ fix x
+ show "h x \<sqsubseteq> f x \<sqinter> g x"
+ proof
+ from hf show "h x \<sqsubseteq> f x" ..
+ from hg show "h x \<sqsubseteq> g x" ..
+ qed
+ qed
+qed
+
+lemma is_sup_fun: "is_sup f g (\<lambda>x. f x \<squnion> g x)" (* FIXME dualize!? *)
+proof
+ show "f \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
+ proof
+ fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..
+ qed
+ show "g \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
+ proof
+ fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..
+ qed
+ fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"
+ show "(\<lambda>x. f x \<squnion> g x) \<sqsubseteq> h"
+ proof
+ fix x
+ show "f x \<squnion> g x \<sqsubseteq> h x"
+ proof
+ from fh show "f x \<sqsubseteq> h x" ..
+ from gh show "g x \<sqsubseteq> h x" ..
+ qed
+ qed
+qed
+
+instance fun :: ("term", lattice) lattice
+proof intro_classes
+ fix f g :: "'a \<Rightarrow> 'b::lattice"
+ show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
+ show "\<exists>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 \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ by (rule meet_equality) (rule is_inf_fun)
+
+theorem join_fun: "f \<squnion> g = (\<lambda>x. f x \<squnion> 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 \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"
+proof -
+ {
+ fix a b c :: "'a::lattice"
+ assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
+ proof
+ have "a \<sqinter> b \<sqsubseteq> a" ..
+ also have "\<dots> \<sqsubseteq> c" .
+ finally show "a \<sqinter> b \<sqsubseteq> c" .
+ show "a \<sqinter> b \<sqsubseteq> b" ..
+ qed
+ } note this [elim?]
+ assume "x \<sqsubseteq> z" hence "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
+ also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
+ also assume "y \<sqsubseteq> w" hence "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
+ also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
+ finally show ?thesis .
+qed
+
+theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
+proof -
+ assume "x \<sqsubseteq> z" hence "dual z \<sqsubseteq> dual x" ..
+ moreover assume "y \<sqsubseteq> w" hence "dual w \<sqsubseteq> dual y" ..
+ ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
+ by (rule meet_mono)
+ hence "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
+ by (simp only: dual_join)
+ thus ?thesis ..
+qed
+
+text {*
+ \medskip A semi-morphisms is a function $f$ that preserves the
+ lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
+ \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively. Any of
+ these properties is equivalent with monotonicity.
+*} (* FIXME dual version !? *)
+
+theorem meet_semimorph:
+ "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
+proof
+ assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
+ fix x y :: "'a::lattice"
+ assume "x \<sqsubseteq> y" hence "x \<sqinter> y = x" ..
+ hence "x = x \<sqinter> y" ..
+ also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
+ also have "\<dots> \<sqsubseteq> f y" ..
+ finally show "f x \<sqsubseteq> f y" .
+next
+ assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+ show "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
+ proof -
+ fix x y
+ show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
+ proof
+ have "x \<sqinter> y \<sqsubseteq> x" .. thus "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
+ have "x \<sqinter> y \<sqsubseteq> y" .. thus "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
+ qed
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/Orders.thy Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,294 @@
+(* Title: HOL/Lattice/Orders.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+header {* Orders *}
+
+theory Orders = Main:
+
+subsection {* Ordered structures *}
+
+text {*
+ We define several classes of ordered structures over some type @{typ
+ 'a} with relation @{text "\<sqsubseteq> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}. For a
+ \emph{quasi-order} that relation is required to be reflexive and
+ transitive, for a \emph{partial order} it also has to be
+ anti-symmetric, while for a \emph{linear order} all elements are
+ required to be related (in either direction).
+*}
+
+axclass leq < "term"
+consts
+ leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
+syntax (symbols)
+ leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
+
+axclass quasi_order < leq
+ leq_refl [intro?]: "x \<sqsubseteq> x"
+ leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+
+axclass partial_order < quasi_order
+ leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+
+axclass linear_order < partial_order
+ leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+
+lemma linear_order_cases:
+ "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"
+ by (insert leq_linear) blast
+
+
+subsection {* Duality *}
+
+text {*
+ The \emph{dual} of an ordered structure is an isomorphic copy of the
+ underlying type, with the @{text \<sqsubseteq>} relation defined as the inverse
+ of the original one.
+*}
+
+datatype 'a dual = dual 'a
+
+consts
+ undual :: "'a dual \<Rightarrow> 'a"
+primrec
+ undual_dual: "undual (dual x) = x"
+
+instance dual :: (leq) leq
+ by intro_classes
+
+defs (overloaded)
+ leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
+
+lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"
+ by (simp add: leq_dual_def)
+
+lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"
+ by (simp add: leq_dual_def)
+
+text {*
+ \medskip Functions @{term dual} and @{term undual} are inverse to
+ each other; this entails the following fundamental properties.
+*}
+
+lemma dual_undual [simp]: "dual (undual x') = x'"
+ by (cases x') simp
+
+lemma undual_dual_id [simp]: "undual o dual = id"
+ by (rule ext) simp
+
+lemma dual_undual_id [simp]: "dual o undual = id"
+ by (rule ext) simp
+
+text {*
+ \medskip Since @{term dual} (and @{term undual}) are both injective
+ and surjective, the basic logical connectives (equality,
+ quantification etc.) are transferred as follows.
+*}
+
+lemma undual_equality [iff?]: "(undual x' = undual y') = (x' = y')"
+ by (cases x', cases y') simp
+
+lemma dual_equality [iff?]: "(dual x = dual y) = (x = y)"
+ by simp
+
+lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual `` A. P x')"
+proof
+ assume a: "\<forall>x \<in> A. P (dual x)"
+ show "\<forall>x' \<in> dual `` A. P x'"
+ proof
+ fix x' assume x': "x' \<in> dual `` A"
+ have "undual x' \<in> A"
+ proof -
+ from x' have "undual x' \<in> undual `` dual `` A" by simp
+ thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
+ qed
+ with a have "P (dual (undual x'))" ..
+ also have "\<dots> = x'" by simp
+ finally show "P x'" .
+ qed
+next
+ assume a: "\<forall>x' \<in> dual `` A. P x'"
+ show "\<forall>x \<in> A. P (dual x)"
+ proof
+ fix x assume "x \<in> A"
+ hence "dual x \<in> dual `` A" by simp
+ with a show "P (dual x)" ..
+ qed
+qed
+
+lemma range_dual [simp]: "dual `` UNIV = UNIV"
+proof (rule surj_range)
+ have "\<And>x'. dual (undual x') = x'" by simp
+ thus "surj dual" by (rule surjI)
+qed
+
+lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"
+proof -
+ have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual `` UNIV. P x')"
+ by (rule dual_ball)
+ thus ?thesis by simp
+qed
+
+lemma dual_ex: "(\<exists>x. P (dual x)) = (\<exists>x'. P x')"
+proof -
+ have "(\<forall>x. \<not> P (dual x)) = (\<forall>x'. \<not> P x')"
+ by (rule dual_all)
+ thus ?thesis by blast
+qed
+
+lemma dual_Collect: "{dual x| x. P (dual x)} = {x'. P x'}"
+proof -
+ have "{dual x| x. P (dual x)} = {x'. \<exists>x''. x' = x'' \<and> P x''}"
+ by (simp only: dual_ex [symmetric])
+ thus ?thesis by blast
+qed
+
+
+subsection {* Transforming orders *}
+
+subsubsection {* Duals *}
+
+text {*
+ The classes of quasi, partial, and linear orders are all closed
+ under formation of dual structures.
+*}
+
+instance dual :: (quasi_order) quasi_order
+proof intro_classes
+ fix x' y' z' :: "'a::quasi_order dual"
+ have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..
+ assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..
+ also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
+ finally show "x' \<sqsubseteq> z'" ..
+qed
+
+instance dual :: (partial_order) partial_order
+proof intro_classes
+ fix x' y' :: "'a::partial_order dual"
+ assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..
+ also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
+ finally show "x' = y'" ..
+qed
+
+instance dual :: (linear_order) linear_order
+proof intro_classes
+ fix x' y' :: "'a::linear_order dual"
+ show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"
+ proof (rule linear_order_cases)
+ assume "undual y' \<sqsubseteq> undual x'"
+ hence "x' \<sqsubseteq> y'" .. thus ?thesis ..
+ next
+ assume "undual x' \<sqsubseteq> undual y'"
+ hence "y' \<sqsubseteq> x'" .. thus ?thesis ..
+ qed
+qed
+
+
+subsubsection {* Binary products \label{sec:prod-order} *}
+
+text {*
+ The classes of quasi and partial orders are closed under binary
+ products. Note that the direct product of linear orders need
+ \emph{not} be linear in general.
+*}
+
+instance * :: (leq, leq) leq
+ by intro_classes
+
+defs (overloaded)
+ leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
+
+lemma leq_prodI [intro?]:
+ "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
+ by (unfold leq_prod_def) blast
+
+lemma leq_prodE [elim?]:
+ "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
+ by (unfold leq_prod_def) blast
+
+instance * :: (quasi_order, quasi_order) quasi_order
+proof intro_classes
+ fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
+ show "p \<sqsubseteq> p"
+ proof
+ show "fst p \<sqsubseteq> fst p" ..
+ show "snd p \<sqsubseteq> snd p" ..
+ qed
+ assume pq: "p \<sqsubseteq> q" and qr: "q \<sqsubseteq> r"
+ show "p \<sqsubseteq> r"
+ proof
+ from pq have "fst p \<sqsubseteq> fst q" ..
+ also from qr have "\<dots> \<sqsubseteq> fst r" ..
+ finally show "fst p \<sqsubseteq> fst r" .
+ from pq have "snd p \<sqsubseteq> snd q" ..
+ also from qr have "\<dots> \<sqsubseteq> snd r" ..
+ finally show "snd p \<sqsubseteq> snd r" .
+ qed
+qed
+
+instance * :: (partial_order, partial_order) partial_order
+proof intro_classes
+ fix p q :: "'a::partial_order \<times> 'b::partial_order"
+ assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
+ show "p = q"
+ proof
+ from pq have "fst p \<sqsubseteq> fst q" ..
+ also from qp have "\<dots> \<sqsubseteq> fst p" ..
+ finally show "fst p = fst q" .
+ from pq have "snd p \<sqsubseteq> snd q" ..
+ also from qp have "\<dots> \<sqsubseteq> snd p" ..
+ finally show "snd p = snd q" .
+ qed
+qed
+
+
+subsubsection {* General products \label{sec:fun-order} *}
+
+text {*
+ The classes of quasi and partial orders are closed under general
+ products (function spaces). Note that the direct product of linear
+ orders need \emph{not} be linear in general.
+*}
+
+instance fun :: ("term", leq) leq
+ by intro_classes
+
+defs (overloaded)
+ leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
+
+lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+ by (unfold leq_fun_def) blast
+
+lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
+ by (unfold leq_fun_def) blast
+
+instance fun :: ("term", quasi_order) quasi_order
+proof intro_classes
+ fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
+ show "f \<sqsubseteq> f"
+ proof
+ fix x show "f x \<sqsubseteq> f x" ..
+ qed
+ assume fg: "f \<sqsubseteq> g" and gh: "g \<sqsubseteq> h"
+ show "f \<sqsubseteq> h"
+ proof
+ fix x from fg have "f x \<sqsubseteq> g x" ..
+ also from gh have "\<dots> \<sqsubseteq> h x" ..
+ finally show "f x \<sqsubseteq> h x" .
+ qed
+qed
+
+instance fun :: ("term", partial_order) partial_order
+proof intro_classes
+ fix f g :: "'a \<Rightarrow> 'b::partial_order"
+ assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
+ show "f = g"
+ proof
+ fix x from fg have "f x \<sqsubseteq> g x" ..
+ also from gf have "\<dots> \<sqsubseteq> f x" ..
+ finally show "f x = g x" .
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/ROOT.ML Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,8 @@
+(* Title: HOL/Lattice/ROOT.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Basic theory of lattices and orders.
+*)
+
+time_use_thy "CompleteLattice";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/document/root.bib Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,48 @@
+
+@InProceedings{Bauer-Wenzel:2000:HB,
+ author = {Gertrud Bauer and Markus Wenzel},
+ title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
+ {I}sabelle/{I}sar},
+ booktitle = {Types for Proofs and Programs: TYPES'99},
+ editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
+ and Jan Smith},
+ series = {LNCS},
+ year = 2000
+}
+
+@Book{Davey-Priestley:1990,
+ author = {B. A. Davey and H. A. Priestley},
+ title = {Introduction to Lattices and Order},
+ publisher = {Cambridge University Press},
+ year = 1990}
+
+@InProceedings{Wenzel:1999:TPHOL,
+ author = {Markus Wenzel},
+ title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+ crossref = {tphols99}}
+
+
+@Manual{Wenzel:2000:axclass,
+ author = {Markus Wenzel},
+ title = {Using Axiomatic Type Classes in Isabelle},
+ year = 2000,
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
+}
+
+@Manual{Wenzel:2000:isar-ref,
+ author = {Markus Wenzel},
+ title = {The {Isabelle/Isar} Reference Manual},
+ year = 2000,
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
+}
+
+@Proceedings{tphols99,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+ editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
+ Paulin, C. and Thery, L.},
+ series = {LNCS},
+ volume = 1690,
+ year = 1999}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lattice/document/root.tex Fri Oct 06 01:04:56 2000 +0200
@@ -0,0 +1,56 @@
+
+% $Id$
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym,pdfsetup}
+\usepackage[only,bigsqcap]{stmaryrd}
+
+\urlstyle{rm}\isabellestyle{it}
+\pagestyle{headings}
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+
+
+\begin{document}
+
+\title{Lattices and Orders in Isabelle/HOL}
+\author{Markus Wenzel \\ TU M\"unchen}
+\maketitle
+
+\begin{abstract}
+ We consider abstract structures of orders and lattices. Many fundamental
+ concepts of lattice theory are developed, including dual structures,
+ properties of bounds versus algebraic laws, lattice operations versus
+ set-theoretic ones etc. We also give example instantiations of lattices and
+ orders, such as direct products and function spaces. Well-known properties
+ are demonstrated, like the Knaster-Tarski Theorem for complete lattices.
+
+ This formal theory development may serve as an example of applying
+ Isabelle/HOL to the domain of mathematical reasoning about ``axiomatic''
+ structures. Apart from the simply-typed classical set-theory of HOL, we
+ employ Isabelle's system of axiomatic type classes for expressing structures
+ and functors in a light-weight manner. Proofs are expressed in the Isar
+ language for readable formal proof, while aiming at its ``best-style'' of
+ representing formal reasoning.
+\end{abstract}
+
+\tableofcontents
+
+\newpage
+{
+ \parindent 0pt\parskip 0.7ex
+ \pagestyle{myheadings}
+ \renewcommand{\isamarkupheader}[1]{\markright{THEORY~``\isabellecontext''}\section{#1}}
+ \input{session}
+}
+
+\nocite{Wenzel:1999:TPHOL}
+\nocite{Wenzel:2000:isar-ref}
+\nocite{Wenzel:2000:axclass}
+\nocite{Bauer-Wenzel:2000:HB}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}