# HG changeset patch # User wenzelm # Date 970787096 -7200 # Node ID 6d3987f3aad93801fe56cbec810349023e5c2cc8 # Parent 9d4d5852eb478708f28fbb27444d9a52f95be8ce * HOL/Lattice: fundamental concepts of lattice theory and order structures; diff -r 9d4d5852eb47 -r 6d3987f3aad9 NEWS --- 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; diff -r 9d4d5852eb47 -r 6d3987f3aad9 src/HOL/IsaMakefile --- 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 diff -r 9d4d5852eb47 -r 6d3987f3aad9 src/HOL/Lattice/Bounds.thy --- /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 \} for two and for any + number of elements. +*} + +constdefs + is_inf :: "'a::partial_order \ 'a \ 'a \ bool" + "is_inf x y inf \ inf \ x \ inf \ y \ (\z. z \ x \ z \ y \ z \ inf)" + + is_sup :: "'a::partial_order \ 'a \ 'a \ bool" + "is_sup x y sup \ x \ sup \ y \ sup \ (\z. x \ z \ y \ z \ sup \ z)" + + is_Inf :: "'a::partial_order set \ 'a \ bool" + "is_Inf A inf \ (\x \ A. inf \ x) \ (\z. (\x \ A. z \ x) \ z \ inf)" + + is_Sup :: "'a::partial_order set \ 'a \ bool" + "is_Sup A sup \ (\x \ A. x \ sup) \ (\z. (\x \ A. x \ z) \ sup \ z)" + +text {* + These definitions entail the following basic properties of boundary + elements. +*} + +lemma is_infI [intro?]: "inf \ x \ inf \ y \ + (\z. z \ x \ z \ y \ z \ inf) \ is_inf x y inf" + by (unfold is_inf_def) blast + +lemma is_inf_greatest [elim?]: + "is_inf x y inf \ z \ x \ z \ y \ z \ inf" + by (unfold is_inf_def) blast + +lemma is_inf_lower [elim?]: + "is_inf x y inf \ (inf \ x \ inf \ y \ C) \ C" + by (unfold is_inf_def) blast + + +lemma is_supI [intro?]: "x \ sup \ y \ sup \ + (\z. x \ z \ y \ z \ sup \ z) \ is_sup x y sup" + by (unfold is_sup_def) blast + +lemma is_sup_least [elim?]: + "is_sup x y sup \ x \ z \ y \ z \ sup \ z" + by (unfold is_sup_def) blast + +lemma is_sup_upper [elim?]: + "is_sup x y sup \ (x \ sup \ y \ sup \ C) \ C" + by (unfold is_sup_def) blast + + +lemma is_InfI [intro?]: "(\x. x \ A \ inf \ x) \ + (\z. (\x \ A. z \ x) \ z \ inf) \ is_Inf A inf" + by (unfold is_Inf_def) blast + +lemma is_Inf_greatest [elim?]: + "is_Inf A inf \ (\x. x \ A \ z \ x) \ z \ inf" + by (unfold is_Inf_def) blast + +lemma is_Inf_lower [dest?]: + "is_Inf A inf \ x \ A \ inf \ x" + by (unfold is_Inf_def) blast + + +lemma is_SupI [intro?]: "(\x. x \ A \ x \ sup) \ + (\z. (\x \ A. x \ z) \ sup \ z) \ is_Sup A sup" + by (unfold is_Sup_def) blast + +lemma is_Sup_least [elim?]: + "is_Sup A sup \ (\x. x \ A \ x \ z) \ sup \ z" + by (unfold is_Sup_def) blast + +lemma is_Sup_upper [dest?]: + "is_Sup A sup \ x \ A \ x \ 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 \ is_inf x y inf' \ 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 \ inf'" + proof (rule is_inf_greatest) + from inf show "inf \ x" .. + from inf show "inf \ y" .. + qed + from inf show "inf' \ inf" + proof (rule is_inf_greatest) + from inf' show "inf' \ x" .. + from inf' show "inf' \ y" .. + qed + qed +qed + +theorem is_sup_uniq: "is_sup x y sup \ is_sup x y sup' \ 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 \ is_Inf A inf' \ 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 \ inf'" + proof (rule is_Inf_greatest) + fix x assume "x \ A" + from inf show "inf \ x" .. + qed + from inf show "inf' \ inf" + proof (rule is_Inf_greatest) + fix x assume "x \ A" + from inf' show "inf' \ x" .. + qed + qed +qed + +theorem is_Sup_uniq: "is_Sup A sup \ is_Sup A sup' \ 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 \ y \ is_inf x y x" +proof - + assume "x \ y" + show ?thesis + proof + show "x \ x" .. + show "x \ y" . + fix z assume "z \ x" and "z \ y" show "z \ x" . + qed +qed + +theorem is_sup_related [elim?]: "x \ y \ is_sup x y y" +proof - + assume "x \ y" + show ?thesis + proof + show "x \ y" . + show "y \ y" .. + fix z assume "x \ z" and "y \ z" + show "y \ 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 \ ?A" by simp + with is_Inf show "inf \ x" .. + have "y \ ?A" by simp + with is_Inf show "inf \ y" .. + fix z assume zx: "z \ x" and zy: "z \ y" + from is_Inf show "z \ inf" + proof (rule is_Inf_greatest) + fix a assume "a \ ?A" + hence "a = x \ a = y" by blast + thus "z \ 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 \ ?A" + hence "a = x \ a = y" by blast + thus "inf \ a" + proof + assume "a = x" + also from is_inf have "inf \ x" .. + finally show ?thesis . + next + assume "a = y" + also from is_inf have "inf \ y" .. + finally show ?thesis . + qed + next + fix z assume z: "\a \ ?A. z \ a" + from is_inf show "z \ inf" + proof (rule is_inf_greatest) + from z show "z \ x" by blast + from z show "z \ 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 \ (dual sup) = is_inf (dual x) (dual y) (dual sup)" + by (rule is_Inf_binary) + also have "\ = 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. \a \ A. a \ b} sup \ is_Sup A sup" +proof - + let ?B = "{b. \a \ A. a \ b}" + assume is_Inf: "is_Inf ?B sup" + show "is_Sup A sup" + proof + fix x assume x: "x \ A" + from is_Inf show "x \ sup" + proof (rule is_Inf_greatest) + fix y assume "y \ ?B" + hence "\a \ A. a \ y" .. + from this x show "x \ y" .. + qed + next + fix z assume "\x \ A. x \ z" + hence "z \ ?B" .. + with is_Inf show "sup \ z" .. + qed +qed + +theorem Sup_Inf: "is_Sup {b. \a \ A. b \ a} inf \ is_Inf A inf" +proof - + assume "is_Sup {b. \a \ A. b \ a} inf" + hence "is_Inf (dual `` {b. \a \ A. dual a \ dual b}) (dual inf)" + by (simp only: dual_Inf dual_leq) + also have "dual `` {b. \a \ A. dual a \ dual b} = {b'. \a' \ dual `` A. a' \ b'}" + by (auto iff: dual_ball dual_Collect) (* FIXME !? *) + finally have "is_Inf \ (dual inf)" . + hence "is_Sup (dual `` A) (dual inf)" + by (rule Inf_Sup) + thus ?thesis .. +qed + +end diff -r 9d4d5852eb47 -r 6d3987f3aad9 src/HOL/Lattice/CompleteLattice.thy --- /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: "\inf. is_Inf A inf" + +theorem ex_Sup: "\sup::'a::complete_lattice. is_Sup A sup" +proof - + from ex_Inf obtain sup where "is_Inf {b. \a\A. a \ b} sup" by blast + hence "is_Sup A sup" by (rule Inf_Sup) + thus ?thesis .. +qed + +text {* + The general @{text \} (meet) and @{text \} (join) operations select + such infimum and supremum elements. +*} + +consts + Meet :: "'a::complete_lattice set \ 'a" + Join :: "'a::complete_lattice set \ 'a" +syntax (symbols) + Meet :: "'a::complete_lattice set \ 'a" ("\_" [90] 90) + Join :: "'a::complete_lattice set \ 'a" ("\_" [90] 90) +defs + Meet_def: "\A \ SOME inf. is_Inf A inf" + Join_def: "\A \ 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 \ \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?]: + "(\a. a \ A \ inf \ a) \ + (\b. \a \ A. b \ a \ b \ inf) \ + \A = inf" + by (rule Meet_equality, rule is_InfI) blast+ + +lemma Join_equality [elim?]: "is_Sup A sup \ \A = sup" +proof (unfold Join_def) + assume "is_Sup A sup" + thus "(SOME sup. is_Sup A sup) = sup" + by (rule some_equality) (rule is_Sup_uniq) +qed + +lemma JoinI [intro?]: + "(\a. a \ A \ a \ sup) \ + (\b. \a \ A. a \ b \ sup \ b) \ + \A = sup" + by (rule Join_equality, rule is_SupI) blast+ + + +text {* + \medskip The @{text \} and @{text \} operations indeed determine + bounds on a complete lattice structure. +*} + +lemma is_Inf_Meet [intro?]: "is_Inf A (\A)" +proof (unfold Meet_def) + from ex_Inf show "is_Inf A (SOME inf. is_Inf A inf)" + by (rule ex_someI) +qed + +lemma Meet_greatest [intro?]: "(\a. a \ A \ x \ a) \ x \ \A" + by (rule is_Inf_greatest, rule is_Inf_Meet) blast + +lemma Meet_lower [intro?]: "a \ A \ \A \ a" + by (rule is_Inf_lower) (rule is_Inf_Meet) + + +lemma is_Sup_Join [intro?]: "is_Sup A (\A)" +proof (unfold Join_def) + from ex_Sup show "is_Sup A (SOME sup. is_Sup A sup)" + by (rule ex_someI) +qed + +lemma Join_least [intro?]: "(\a. a \ A \ a \ x) \ \A \ x" + by (rule is_Sup_least, rule is_Sup_Join) blast +lemma Join_lower [intro?]: "a \ A \ a \ \A" + by (rule is_Sup_upper) (rule is_Sup_Join) + + +subsection {* The Knaster-Tarski Theorem *} + +text {* + The Knaster-Tarski Theorem (in its simplest formulation) states that + any monotone function on a complete lattice has a least fixed-point + (see \cite[pages 93--94]{Davey-Priestley:1990} for example). This + is a consequence of the basic boundary properties of the complete + lattice operations. +*} + +theorem Knaster_Tarski: + "(\x y. x \ y \ f x \ f y) \ \a::'a::complete_lattice. f a = a" +proof + assume mono: "\x y. x \ y \ f x \ f y" + let ?H = "{u. f u \ u}" let ?a = "\?H" + have ge: "f ?a \ ?a" + proof + fix x assume x: "x \ ?H" + hence "?a \ x" .. + hence "f ?a \ f x" by (rule mono) + also from x have "... \ x" .. + finally show "f ?a \ x" . + qed + also have "?a \ f ?a" + proof + from ge have "f (f ?a) \ f ?a" by (rule mono) + 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" ("\") + "\ \ \UNIV" + top :: "'a::complete_lattice" ("\") + "\ \ \UNIV" + +lemma bottom_least [intro?]: "\ \ x" +proof (unfold bottom_def) + have "x \ UNIV" .. + thus "\UNIV \ x" .. +qed + +lemma bottomI [intro?]: "(\a. x \ a) \ \ = x" +proof (unfold bottom_def) + assume "\a. x \ a" + show "\UNIV = x" + proof + fix a show "x \ a" . + next + fix b :: "'a::complete_lattice" + assume b: "\a \ UNIV. b \ a" + have "x \ UNIV" .. + with b show "b \ x" .. + qed +qed + +lemma top_greatest [intro?]: "x \ \" +proof (unfold top_def) + have "x \ UNIV" .. + thus "x \ \UNIV" .. +qed + +lemma topI [intro?]: "(\a. a \ x) \ \ = x" +proof (unfold top_def) + assume "\a. a \ x" + show "\UNIV = x" + proof + fix a show "a \ x" . + next + fix b :: "'a::complete_lattice" + assume b: "\a \ UNIV. a \ b" + have "x \ UNIV" .. + with b show "x \ b" .. + qed +qed + + +subsection {* Duality *} + +text {* + The class of complete lattices is closed under formation of dual + structures. +*} + +instance dual :: (complete_lattice) complete_lattice +proof intro_classes + fix A' :: "'a::complete_lattice dual set" + show "\inf'. is_Inf A' inf'" + proof - + have "\sup. is_Sup (undual `` A') sup" by (rule ex_Sup) + hence "\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 \} and @{text \} operations are dual to each + other. +*} + +theorem dual_Meet [intro?]: "dual (\A) = \(dual `` A)" +proof - + from is_Inf_Meet have "is_Sup (dual `` A) (dual (\A))" .. + hence "\(dual `` A) = dual (\A)" .. + thus ?thesis .. +qed + +theorem dual_Join [intro?]: "dual (\A) = \(dual `` A)" +proof - + from is_Sup_Join have "is_Inf (dual `` A) (dual (\A))" .. + hence "\(dual `` A) = dual (\A)" .. + thus ?thesis .. +qed + +text {* + Likewise are @{text \} and @{text \} duals of each other. +*} + +theorem dual_bottom [intro?]: "dual \ = \" +proof - + have "\ = dual \" + proof + fix a' have "\