author wenzelm Fri, 06 Oct 2000 01:04:56 +0200 changeset 10157 6d3987f3aad9 parent 10156 9d4d5852eb47 child 10158 00fdd5c330ea
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
 NEWS file | annotate | diff | comparison | revisions src/HOL/IsaMakefile file | annotate | diff | comparison | revisions src/HOL/Lattice/Bounds.thy file | annotate | diff | comparison | revisions src/HOL/Lattice/CompleteLattice.thy file | annotate | diff | comparison | revisions src/HOL/Lattice/Lattice.thy file | annotate | diff | comparison | revisions src/HOL/Lattice/Orders.thy file | annotate | diff | comparison | revisions src/HOL/Lattice/ROOT.ML file | annotate | diff | comparison | revisions src/HOL/Lattice/document/root.bib file | annotate | diff | comparison | revisions src/HOL/Lattice/document/root.tex file | annotate | diff | comparison | revisions
--- 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) + Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_"  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}
+
+\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
+  \renewcommand{\isamarkupheader}{\markright{THEORY~\isabellecontext''}\section{#1}}
+\end{document}