# HG changeset patch # User wenzelm # Date 1451496339 -3600 # Node ID 2461779da2b8d0ac75d92994a6ccff1e08360563 # Parent a63a11b0933591f5867ffe3ec3fba8ac5f22a8e0 isabelle update_cartouches -c -t; diff -r a63a11b09335 -r 2461779da2b8 src/HOL/Lattice/Bounds.thy --- a/src/HOL/Lattice/Bounds.thy Wed Dec 30 18:24:36 2015 +0100 +++ b/src/HOL/Lattice/Bounds.thy Wed Dec 30 18:25:39 2015 +0100 @@ -2,19 +2,19 @@ Author: Markus Wenzel, TU Muenchen *) -section {* Bounds *} +section \Bounds\ theory Bounds imports Orders begin hide_const (open) inf sup -subsection {* Infimum and supremum *} +subsection \Infimum and supremum\ -text {* +text \ Given a partial order, we define infimum (greatest lower bound) and - supremum (least upper bound) wrt.\ @{text \} for two and for any + supremum (least upper bound) wrt.\ \\\ for two and for any number of elements. -*} +\ definition is_inf :: "'a::partial_order \ 'a \ 'a \ bool" where @@ -32,10 +32,10 @@ is_Sup :: "'a::partial_order set \ 'a \ bool" where "is_Sup A sup = ((\x \ A. x \ sup) \ (\z. (\x \ A. x \ z) \ sup \ z))" -text {* +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" @@ -89,11 +89,11 @@ by (unfold is_Sup_def) blast -subsection {* Duality *} +subsection \Duality\ -text {* +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" @@ -112,12 +112,12 @@ by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq) -subsection {* Uniqueness *} +subsection \Uniqueness\ -text {* +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 - @@ -180,11 +180,11 @@ qed -subsection {* Related elements *} +subsection \Related elements\ -text {* +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 - @@ -210,11 +210,11 @@ qed -subsection {* General versus binary bounds \label{sec:gen-bin-bounds} *} +subsection \General versus binary bounds \label{sec:gen-bin-bounds}\ -text {* +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 - @@ -284,14 +284,14 @@ qed -subsection {* Connecting general bounds \label{sec:connect-bounds} *} +subsection \Connecting general bounds \label{sec:connect-bounds}\ -text {* +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 - diff -r a63a11b09335 -r 2461779da2b8 src/HOL/Lattice/CompleteLattice.thy --- a/src/HOL/Lattice/CompleteLattice.thy Wed Dec 30 18:24:36 2015 +0100 +++ b/src/HOL/Lattice/CompleteLattice.thy Wed Dec 30 18:25:39 2015 +0100 @@ -2,18 +2,18 @@ Author: Markus Wenzel, TU Muenchen *) -section {* Complete lattices *} +section \Complete lattices\ theory CompleteLattice imports Lattice begin -subsection {* Complete lattice operations *} +subsection \Complete lattice operations\ -text {* +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}). -*} +\ class complete_lattice = assumes ex_Inf: "\inf. is_Inf A inf" @@ -25,10 +25,10 @@ then show ?thesis .. qed -text {* - The general @{text \} (meet) and @{text \} (join) operations select +text \ + The general \\\ (meet) and \\\ (join) operations select such infimum and supremum elements. -*} +\ definition Meet :: "'a::complete_lattice set \ 'a" ("\_" [90] 90) where @@ -37,16 +37,16 @@ Join :: "'a::complete_lattice set \ 'a" ("\_" [90] 90) where "\A = (THE sup. is_Sup A sup)" -text {* +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" then show "(THE inf. is_Inf A inf) = inf" - by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`]) + by (rule the_equality) (rule is_Inf_uniq [OF _ \is_Inf A inf\]) qed lemma MeetI [intro?]: @@ -59,7 +59,7 @@ proof (unfold Join_def) assume "is_Sup A sup" then show "(THE sup. is_Sup A sup) = sup" - by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`]) + by (rule the_equality) (rule is_Sup_uniq [OF _ \is_Sup A sup\]) qed lemma JoinI [intro?]: @@ -69,16 +69,16 @@ by (rule Join_equality, rule is_SupI) blast+ -text {* - \medskip The @{text \} and @{text \} operations indeed determine +text \ + \medskip The \\\ and \\\ 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 obtain inf where "is_Inf A inf" .. then show "is_Inf A (THE inf. is_Inf A inf)" - by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`]) + by (rule theI) (rule is_Inf_uniq [OF _ \is_Inf A inf\]) qed lemma Meet_greatest [intro?]: "(\a. a \ A \ x \ a) \ x \ \A" @@ -92,7 +92,7 @@ proof (unfold Join_def) from ex_Sup obtain sup where "is_Sup A sup" .. then show "is_Sup A (THE sup. is_Sup A sup)" - by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`]) + by (rule theI) (rule is_Sup_uniq [OF _ \is_Sup A sup\]) qed lemma Join_least [intro?]: "(\a. a \ A \ a \ x) \ \A \ x" @@ -101,15 +101,15 @@ by (rule is_Sup_upper) (rule is_Sup_Join) -subsection {* The Knaster-Tarski Theorem *} +subsection \The Knaster-Tarski Theorem\ -text {* +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: assumes mono: "\x y. x \ y \ f x \ f y" @@ -176,12 +176,12 @@ qed -subsection {* Bottom and top elements *} +subsection \Bottom and top elements\ -text {* +text \ With general bounds available, complete lattices also have least and greatest elements. -*} +\ definition bottom :: "'a::complete_lattice" ("\") where @@ -232,12 +232,12 @@ qed -subsection {* Duality *} +subsection \Duality\ -text {* +text \ The class of complete lattices is closed under formation of dual structures. -*} +\ instance dual :: (complete_lattice) complete_lattice proof @@ -250,10 +250,10 @@ qed qed -text {* - Apparently, the @{text \} and @{text \} operations are dual to each +text \ + Apparently, the \\\ and \\\ operations are dual to each other. -*} +\ theorem dual_Meet [intro?]: "dual (\A) = \(dual ` A)" proof - @@ -269,9 +269,9 @@ then show ?thesis .. qed -text {* - Likewise are @{text \} and @{text \} duals of each other. -*} +text \ + Likewise are \\\ and \\\ duals of each other. +\ theorem dual_bottom [intro?]: "dual \ = \" proof - @@ -296,14 +296,14 @@ qed -subsection {* Complete lattices are lattices *} +subsection \Complete lattices are lattices\ -text {* +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 (\{x, y})" proof - @@ -331,12 +331,12 @@ by (rule join_equality) (rule is_sup_binary) -subsection {* Complete lattices and set-theory operations *} +subsection \Complete lattices and set-theory operations\ -text {* +text \ The complete lattice operations are (anti) monotone wrt.\ set inclusion. -*} +\ theorem Meet_subset_antimono: "A \ B \ \B \ \A" proof (rule Meet_greatest) @@ -355,9 +355,9 @@ then show ?thesis by (simp only: dual_leq) qed -text {* +text \ Bounds over unions of sets may be obtained separately. -*} +\ theorem Meet_Un: "\(A \ B) = \A \ \B" proof @@ -404,9 +404,9 @@ finally show ?thesis .. qed -text {* +text \ Bounds over singleton sets are trivial. -*} +\ theorem Meet_singleton: "\{x} = x" proof @@ -425,9 +425,9 @@ finally show ?thesis .. qed -text {* +text \ Bounds over the empty and universal set correspond to each other. -*} +\ theorem Meet_empty: "\{} = \UNIV" proof diff -r a63a11b09335 -r 2461779da2b8 src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Wed Dec 30 18:24:36 2015 +0100 +++ b/src/HOL/Lattice/Lattice.thy Wed Dec 30 18:25:39 2015 +0100 @@ -2,26 +2,26 @@ Author: Markus Wenzel, TU Muenchen *) -section {* Lattices *} +section \Lattices\ theory Lattice imports Bounds begin -subsection {* Lattice operations *} +subsection \Lattice operations\ -text {* +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). -*} +\ class lattice = assumes ex_inf: "\inf. is_inf x y inf" assumes ex_sup: "\sup. is_sup x y sup" -text {* - The @{text \} (meet) and @{text \} (join) operations select such +text \ + The \\\ (meet) and \\\ (join) operations select such infimum and supremum elements. -*} +\ definition meet :: "'a::lattice \ 'a \ 'a" (infixl "\" 70) where @@ -30,16 +30,16 @@ join :: "'a::lattice \ 'a \ 'a" (infixl "\" 65) where "x \ y = (THE sup. is_sup x y sup)" -text {* +text \ Due to unique existence of bounds, the lattice operations may be exhibited as follows. -*} +\ lemma meet_equality [elim?]: "is_inf x y inf \ x \ y = inf" proof (unfold meet_def) assume "is_inf x y inf" then show "(THE inf. is_inf x y inf) = inf" - by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`]) + by (rule the_equality) (rule is_inf_uniq [OF _ \is_inf x y inf\]) qed lemma meetI [intro?]: @@ -50,7 +50,7 @@ proof (unfold join_def) assume "is_sup x y sup" then show "(THE sup. is_sup x y sup) = sup" - by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`]) + by (rule the_equality) (rule is_sup_uniq [OF _ \is_sup x y sup\]) qed lemma joinI [intro?]: "x \ sup \ y \ sup \ @@ -58,16 +58,16 @@ by (rule join_equality, rule is_supI) blast+ -text {* - \medskip The @{text \} and @{text \} operations indeed determine +text \ + \medskip The \\\ and \\\ operations indeed determine bounds on a lattice structure. -*} +\ lemma is_inf_meet [intro?]: "is_inf x y (x \ y)" proof (unfold meet_def) from ex_inf obtain inf where "is_inf x y inf" .. then show "is_inf x y (THE inf. is_inf x y inf)" - by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`]) + by (rule theI) (rule is_inf_uniq [OF _ \is_inf x y inf\]) qed lemma meet_greatest [intro?]: "z \ x \ z \ y \ z \ x \ y" @@ -84,7 +84,7 @@ proof (unfold join_def) from ex_sup obtain sup where "is_sup x y sup" .. then show "is_sup x y (THE sup. is_sup x y sup)" - by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`]) + by (rule theI) (rule is_sup_uniq [OF _ \is_sup x y sup\]) qed lemma join_least [intro?]: "x \ z \ y \ z \ x \ y \ z" @@ -97,14 +97,14 @@ by (rule is_sup_upper) (rule is_sup_join) -subsection {* Duality *} +subsection \Duality\ -text {* +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 @@ -125,10 +125,10 @@ qed qed -text {* - Apparently, the @{text \} and @{text \} operations are dual to each +text \ + Apparently, the \\\ and \\\ operations are dual to each other. -*} +\ theorem dual_meet [intro?]: "dual (x \ y) = dual x \ dual y" proof - @@ -145,13 +145,13 @@ qed -subsection {* Algebraic properties \label{sec:lattice-algebra} *} +subsection \Algebraic properties \label{sec:lattice-algebra}\ -text {* - The @{text \} and @{text \} operations have the following +text \ + The \\\ and \\\ operations have the following characteristic algebraic properties: associative (A), commutative (C), and absorptive (AB). -*} +\ theorem meet_assoc: "(x \ y) \ z = x \ (y \ z)" proof @@ -239,10 +239,10 @@ then show ?thesis .. qed -text {* +text \ \medskip Some further algebraic properties hold as well. The property idempotent (I) is a basic algebraic consequence of (AB). -*} +\ theorem meet_idem: "x \ x = x" proof - @@ -260,9 +260,9 @@ then show ?thesis .. qed -text {* +text \ Meet and join are trivial for related elements. -*} +\ theorem meet_related [elim?]: "x \ y \ x \ y = x" proof @@ -283,12 +283,12 @@ qed -subsection {* Order versus algebraic structure *} +subsection \Order versus algebraic structure\ -text {* - The @{text \} and @{text \} operations are connected with the - underlying @{text \} relation in a canonical manner. -*} +text \ + The \\\ and \\\ operations are connected with the + underlying \\\ relation in a canonical manner. +\ theorem meet_connection: "(x \ y) = (x \ y = x)" proof @@ -312,28 +312,28 @@ finally show "x \ y" . qed -text {* +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 \} and @{text \} + Given a structure with binary operations \\\ and \\\ such that (A), (C), and (AB) hold (cf.\ \S\ref{sec:lattice-algebra}). This structure represents a lattice, if the relation @{term "x \ y"} is defined as @{term "x \ y = x"} (alternatively as @{term "x \ y = y"}). Furthermore, infimum and supremum with respect to this ordering coincide with the original - @{text \} and @{text \} operations. -*} + \\\ and \\\ operations. +\ -subsection {* Example instances *} +subsection \Example instances\ -subsubsection {* Linear orders *} +subsubsection \Linear orders\ -text {* +text \ Linear orders with @{term minimum} and @{term maximum} operations are a (degenerate) example of lattice structures. -*} +\ definition minimum :: "'a::linear_order \ 'a \ 'a" where @@ -367,10 +367,10 @@ from is_sup_maximum show "\sup. is_sup x y sup" .. qed -text {* +text \ The lattice operations on linear orders indeed coincide with @{term minimum} and @{term maximum}. -*} +\ theorem meet_mimimum: "x \ y = minimum x y" by (rule meet_equality) (rule is_inf_minimum) @@ -380,12 +380,12 @@ -subsubsection {* Binary products *} +subsubsection \Binary products\ -text {* +text \ The class of lattices is closed under direct binary products (cf.\ \S\ref{sec:prod-order}). -*} +\ lemma is_inf_prod: "is_inf p q (fst p \ fst q, snd p \ snd q)" proof @@ -456,10 +456,10 @@ from is_sup_prod show "\sup. is_sup p q sup" .. qed -text {* +text \ The lattice operations on a binary product structure indeed coincide with the products of the original ones. -*} +\ theorem meet_prod: "p \ q = (fst p \ fst q, snd p \ snd q)" by (rule meet_equality) (rule is_inf_prod) @@ -468,12 +468,12 @@ by (rule join_equality) (rule is_sup_prod) -subsubsection {* General products *} +subsubsection \General products\ -text {* +text \ The class of lattices is closed under general products (function spaces) as well (cf.\ \S\ref{sec:fun-order}). -*} +\ lemma is_inf_fun: "is_inf f g (\x. f x \ g x)" proof @@ -526,10 +526,10 @@ show "\sup. is_sup f g sup" by rule (rule is_sup_fun) qed -text {* +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 \ g = (\x. f x \ g x)" by (rule meet_equality) (rule is_inf_fun) @@ -538,13 +538,13 @@ by (rule join_equality) (rule is_sup_fun) -subsection {* Monotonicity and semi-morphisms *} +subsection \Monotonicity and semi-morphisms\ -text {* +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 \ z \ y \ w \ x \ y \ z \ w" proof - @@ -576,12 +576,12 @@ then show ?thesis .. qed -text {* - \medskip A semi-morphisms is a function @{text f} that preserves the +text \ + \medskip A semi-morphisms is a function \f\ that preserves the lattice operations in the following manner: @{term "f (x \ y) \ f x \ f y"} and @{term "f x \ f y \ f (x \ y)"}, respectively. Any of these properties is equivalent with monotonicity. -*} +\ theorem meet_semimorph: "(\x y. f (x \ y) \ f x \