(* Title: HOL/Lattice/Lattice.thy Author: Markus Wenzel, TU Muenchen *) section ‹Lattices› theory Lattice imports Bounds begin 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). › class lattice = assumes ex_inf: "∃inf. is_inf x y inf" assumes ex_sup: "∃sup. is_sup x y sup" text ‹ The ‹⊓› (meet) and ‹⊔› (join) operations select such infimum and supremum elements. › definition meet :: "'a::lattice ⇒ 'a ⇒ 'a" (infixl "⊓" 70) where "x ⊓ y = (THE inf. is_inf x y inf)" definition join :: "'a::lattice ⇒ 'a ⇒ 'a" (infixl "⊔" 65) where "x ⊔ y = (THE 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 ⟹ 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›]) qed lemma meetI [intro?]: "inf ⊑ x ⟹ inf ⊑ y ⟹ (⋀z. z ⊑ x ⟹ z ⊑ y ⟹ z ⊑ inf) ⟹ x ⊓ y = inf" by (rule meet_equality, rule is_infI) blast+ lemma join_equality [elim?]: "is_sup x y sup ⟹ x ⊔ y = sup" 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›]) qed lemma joinI [intro?]: "x ⊑ sup ⟹ y ⊑ sup ⟹ (⋀z. x ⊑ z ⟹ y ⊑ z ⟹ sup ⊑ z) ⟹ x ⊔ y = sup" by (rule join_equality, rule is_supI) blast+ 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›]) qed lemma meet_greatest [intro?]: "z ⊑ x ⟹ z ⊑ y ⟹ z ⊑ x ⊓ y" by (rule is_inf_greatest) (rule is_inf_meet) lemma meet_lower1 [intro?]: "x ⊓ y ⊑ x" by (rule is_inf_lower) (rule is_inf_meet) lemma meet_lower2 [intro?]: "x ⊓ y ⊑ y" by (rule is_inf_lower) (rule is_inf_meet) lemma is_sup_join [intro?]: "is_sup x y (x ⊔ y)" 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›]) qed lemma join_least [intro?]: "x ⊑ z ⟹ y ⊑ z ⟹ x ⊔ y ⊑ z" by (rule is_sup_least) (rule is_sup_join) lemma join_upper1 [intro?]: "x ⊑ x ⊔ y" by (rule is_sup_upper) (rule is_sup_join) lemma join_upper2 [intro?]: "y ⊑ x ⊔ 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 fix x' y' :: "'a::lattice dual" show "∃inf'. is_inf x' y' inf'" proof - have "∃sup. is_sup (undual x') (undual y') sup" by (rule ex_sup) then have "∃sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)" by (simp only: dual_inf) then show ?thesis by (simp add: dual_ex [symmetric]) qed show "∃sup'. is_sup x' y' sup'" proof - have "∃inf. is_inf (undual x') (undual y') inf" by (rule ex_inf) then have "∃inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)" by (simp only: dual_sup) then show ?thesis by (simp add: dual_ex [symmetric]) qed qed text ‹ Apparently, the ‹⊓› and ‹⊔› operations are dual to each other. › theorem dual_meet [intro?]: "dual (x ⊓ y) = dual x ⊔ dual y" proof - from is_inf_meet have "is_sup (dual x) (dual y) (dual (x ⊓ y))" .. then have "dual x ⊔ dual y = dual (x ⊓ y)" .. then show ?thesis .. qed theorem dual_join [intro?]: "dual (x ⊔ y) = dual x ⊓ dual y" proof - from is_sup_join have "is_inf (dual x) (dual y) (dual (x ⊔ y))" .. then have "dual x ⊓ dual y = dual (x ⊔ y)" .. then show ?thesis .. qed subsection ‹Algebraic properties \label{sec:lattice-algebra}› 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 show "x ⊓ (y ⊓ z) ⊑ x ⊓ y" proof show "x ⊓ (y ⊓ z) ⊑ x" .. show "x ⊓ (y ⊓ z) ⊑ y" proof - have "x ⊓ (y ⊓ z) ⊑ y ⊓ z" .. also have "… ⊑ y" .. finally show ?thesis . qed qed show "x ⊓ (y ⊓ z) ⊑ z" proof - have "x ⊓ (y ⊓ z) ⊑ y ⊓ z" .. also have "… ⊑ z" .. finally show ?thesis . qed fix w assume "w ⊑ x ⊓ y" and "w ⊑ z" show "w ⊑ x ⊓ (y ⊓ z)" proof show "w ⊑ x" proof - have "w ⊑ x ⊓ y" by fact also have "… ⊑ x" .. finally show ?thesis . qed show "w ⊑ y ⊓ z" proof show "w ⊑ y" proof - have "w ⊑ x ⊓ y" by fact also have "… ⊑ y" .. finally show ?thesis . qed show "w ⊑ z" by fact qed qed qed theorem join_assoc: "(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)" proof - have "dual ((x ⊔ y) ⊔ z) = (dual x ⊓ dual y) ⊓ dual z" by (simp only: dual_join) also have "… = dual x ⊓ (dual y ⊓ dual z)" by (rule meet_assoc) also have "… = dual (x ⊔ (y ⊔ z))" by (simp only: dual_join) finally show ?thesis .. qed theorem meet_commute: "x ⊓ y = y ⊓ x" proof show "y ⊓ x ⊑ x" .. show "y ⊓ x ⊑ y" .. fix z assume "z ⊑ y" and "z ⊑ x" then show "z ⊑ y ⊓ x" .. qed theorem join_commute: "x ⊔ y = y ⊔ x" proof - have "dual (x ⊔ y) = dual x ⊓ dual y" .. also have "… = dual y ⊓ dual x" by (rule meet_commute) also have "… = dual (y ⊔ x)" by (simp only: dual_join) finally show ?thesis .. qed theorem meet_join_absorb: "x ⊓ (x ⊔ y) = x" proof show "x ⊑ x" .. show "x ⊑ x ⊔ y" .. fix z assume "z ⊑ x" and "z ⊑ x ⊔ y" show "z ⊑ x" by fact qed theorem join_meet_absorb: "x ⊔ (x ⊓ y) = x" proof - have "dual x ⊓ (dual x ⊔ dual y) = dual x" by (rule meet_join_absorb) then have "dual (x ⊔ (x ⊓ y)) = dual x" by (simp only: dual_meet dual_join) then show ?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 ⊓ x = x" proof - have "x ⊓ (x ⊔ (x ⊓ x)) = x" by (rule meet_join_absorb) also have "x ⊔ (x ⊓ x) = x" by (rule join_meet_absorb) finally show ?thesis . qed theorem join_idem: "x ⊔ x = x" proof - have "dual x ⊓ dual x = dual x" by (rule meet_idem) then have "dual (x ⊔ x) = dual x" by (simp only: dual_join) then show ?thesis .. qed text ‹ Meet and join are trivial for related elements. › theorem [elim?]: "x ⊑ y ⟹ x ⊓ y = x" proof assume "x ⊑ y" show "x ⊑ x" .. show "x ⊑ y" by fact fix z assume "z ⊑ x" and "z ⊑ y" show "z ⊑ x" by fact qed theorem [elim?]: "x ⊑ y ⟹ x ⊔ y = y" proof - assume "x ⊑ y" then have "dual y ⊑ dual x" .. then have "dual y ⊓ dual x = dual y" by (rule meet_related) also have "dual y ⊓ dual x = dual (y ⊔ x)" by (simp only: dual_join) also have "y ⊔ x = x ⊔ y" by (rule join_commute) finally show ?thesis .. qed subsection ‹Order versus algebraic structure› text ‹ The ‹⊓› and ‹⊔› operations are connected with the underlying ‹⊑› relation in a canonical manner. › theorem meet_connection: "(x ⊑ y) = (x ⊓ y = x)" proof assume "x ⊑ y" then have "is_inf x y x" .. then show "x ⊓ y = x" .. next have "x ⊓ y ⊑ y" .. also assume "x ⊓ y = x" finally show "x ⊑ y" . qed theorem join_connection: "(x ⊑ y) = (x ⊔ y = y)" proof assume "x ⊑ y" then have "is_sup x y y" .. then show "x ⊔ y = y" .. next have "x ⊑ x ⊔ y" .. also assume "x ⊔ y = y" finally show "x ⊑ 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 ‹⊓› 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 ‹⊓› and ‹⊔› operations. › subsection ‹Example instances› subsubsection ‹Linear orders› 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 "minimum x y = (if x ⊑ y then x else y)" definition maximum :: "'a::linear_order ⇒ 'a ⇒ 'a" where "maximum x y = (if x ⊑ 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 ⊑ x" by (auto simp add: minimum_def) from leq_linear show "?min ⊑ y" by (auto simp add: minimum_def) fix z assume "z ⊑ x" and "z ⊑ y" with leq_linear show "z ⊑ ?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 ⊑ ?max" by (auto simp add: maximum_def) from leq_linear show "y ⊑ ?max" by (auto simp add: maximum_def) fix z assume "x ⊑ z" and "y ⊑ z" with leq_linear show "?max ⊑ z" by (auto simp add: maximum_def) qed instance linear_order ⊆ lattice proof fix x y :: "'a::linear_order" from is_inf_minimum show "∃inf. is_inf x y inf" .. from is_sup_maximum show "∃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 ⊓ y = minimum x y" by (rule meet_equality) (rule is_inf_minimum) theorem meet_maximum: "x ⊔ 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.\ \S\ref{sec:prod-order}). › lemma is_inf_prod: "is_inf p q (fst p ⊓ fst q, snd p ⊓ snd q)" proof show "(fst p ⊓ fst q, snd p ⊓ snd q) ⊑ p" proof - have "fst p ⊓ fst q ⊑ fst p" .. moreover have "snd p ⊓ snd q ⊑ snd p" .. ultimately show ?thesis by (simp add: leq_prod_def) qed show "(fst p ⊓ fst q, snd p ⊓ snd q) ⊑ q" proof - have "fst p ⊓ fst q ⊑ fst q" .. moreover have "snd p ⊓ snd q ⊑ snd q" .. ultimately show ?thesis by (simp add: leq_prod_def) qed fix r assume rp: "r ⊑ p" and rq: "r ⊑ q" show "r ⊑ (fst p ⊓ fst q, snd p ⊓ snd q)" proof - have "fst r ⊑ fst p ⊓ fst q" proof from rp show "fst r ⊑ fst p" by (simp add: leq_prod_def) from rq show "fst r ⊑ fst q" by (simp add: leq_prod_def) qed moreover have "snd r ⊑ snd p ⊓ snd q" proof from rp show "snd r ⊑ snd p" by (simp add: leq_prod_def) from rq show "snd r ⊑ 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 ⊔ fst q, snd p ⊔ snd q)" (* FIXME dualize!? *) proof show "p ⊑ (fst p ⊔ fst q, snd p ⊔ snd q)" proof - have "fst p ⊑ fst p ⊔ fst q" .. moreover have "snd p ⊑ snd p ⊔ snd q" .. ultimately show ?thesis by (simp add: leq_prod_def) qed show "q ⊑ (fst p ⊔ fst q, snd p ⊔ snd q)" proof - have "fst q ⊑ fst p ⊔ fst q" .. moreover have "snd q ⊑ snd p ⊔ snd q" .. ultimately show ?thesis by (simp add: leq_prod_def) qed fix r assume "pr": "p ⊑ r" and qr: "q ⊑ r" show "(fst p ⊔ fst q, snd p ⊔ snd q) ⊑ r" proof - have "fst p ⊔ fst q ⊑ fst r" proof from "pr" show "fst p ⊑ fst r" by (simp add: leq_prod_def) from qr show "fst q ⊑ fst r" by (simp add: leq_prod_def) qed moreover have "snd p ⊔ snd q ⊑ snd r" proof from "pr" show "snd p ⊑ snd r" by (simp add: leq_prod_def) from qr show "snd q ⊑ snd r" by (simp add: leq_prod_def) qed ultimately show ?thesis by (simp add: leq_prod_def) qed qed instance prod :: (lattice, lattice) lattice proof fix p q :: "'a::lattice × 'b::lattice" from is_inf_prod show "∃inf. is_inf p q inf" .. from is_sup_prod show "∃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 ⊓ q = (fst p ⊓ fst q, snd p ⊓ snd q)" by (rule meet_equality) (rule is_inf_prod) theorem join_prod: "p ⊔ q = (fst p ⊔ fst q, snd p ⊔ 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.\ \S\ref{sec:fun-order}). › lemma is_inf_fun: "is_inf f g (λx. f x ⊓ g x)" proof show "(λx. f x ⊓ g x) ⊑ f" proof fix x show "f x ⊓ g x ⊑ f x" .. qed show "(λx. f x ⊓ g x) ⊑ g" proof fix x show "f x ⊓ g x ⊑ g x" .. qed fix h assume hf: "h ⊑ f" and hg: "h ⊑ g" show "h ⊑ (λx. f x ⊓ g x)" proof fix x show "h x ⊑ f x ⊓ g x" proof from hf show "h x ⊑ f x" .. from hg show "h x ⊑ g x" .. qed qed qed lemma is_sup_fun: "is_sup f g (λx. f x ⊔ g x)" (* FIXME dualize!? *) proof show "f ⊑ (λx. f x ⊔ g x)" proof fix x show "f x ⊑ f x ⊔ g x" .. qed show "g ⊑ (λx. f x ⊔ g x)" proof fix x show "g x ⊑ f x ⊔ g x" .. qed fix h assume fh: "f ⊑ h" and gh: "g ⊑ h" show "(λx. f x ⊔ g x) ⊑ h" proof fix x show "f x ⊔ g x ⊑ h x" proof from fh show "f x ⊑ h x" .. from gh show "g x ⊑ h x" .. qed qed qed instance "fun" :: (type, lattice) lattice proof fix f g :: "'a ⇒ 'b::lattice" show "∃inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from … show … .."} does not work!? unification incompleteness!? *) show "∃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 ⊓ g = (λx. f x ⊓ g x)" by (rule meet_equality) (rule is_inf_fun) theorem join_fun: "f ⊔ g = (λx. f x ⊔ 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 ⊑ z ⟹ y ⊑ w ⟹ x ⊓ y ⊑ z ⊓ w" proof - { fix a b c :: "'a::lattice" assume "a ⊑ c" have "a ⊓ b ⊑ c ⊓ b" proof have "a ⊓ b ⊑ a" .. also have "… ⊑ c" by fact finally show "a ⊓ b ⊑ c" . show "a ⊓ b ⊑ b" .. qed } note this [elim?] assume "x ⊑ z" then have "x ⊓ y ⊑ z ⊓ y" .. also have "… = y ⊓ z" by (rule meet_commute) also assume "y ⊑ w" then have "y ⊓ z ⊑ w ⊓ z" .. also have "… = z ⊓ w" by (rule meet_commute) finally show ?thesis . qed theorem join_mono: "x ⊑ z ⟹ y ⊑ w ⟹ x ⊔ y ⊑ z ⊔ w" proof - assume "x ⊑ z" then have "dual z ⊑ dual x" .. moreover assume "y ⊑ w" then have "dual w ⊑ dual y" .. ultimately have "dual z ⊓ dual w ⊑ dual x ⊓ dual y" by (rule meet_mono) then have "dual (z ⊔ w) ⊑ dual (x ⊔ y)" by (simp only: dual_join) then show ?thesis .. qed 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 ⊓ f y) ≡ (⋀x y. x ⊑ y ⟹ f x ⊑ f y)" proof assume morph: "⋀x y. f (x ⊓ y) ⊑ f x ⊓ f y" fix x y :: "'a::lattice" assume "x ⊑ y" then have "x ⊓ y = x" .. then have "x = x ⊓ y" .. also have "f … ⊑ f x ⊓ f y" by (rule morph) also have "… ⊑ f y" .. finally show "f x ⊑ f y" . next assume mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y" show "⋀x y. f (x ⊓ y) ⊑ f x ⊓ f y" proof - fix x y show "f (x ⊓ y) ⊑ f x ⊓ f y" proof have "x ⊓ y ⊑ x" .. then show "f (x ⊓ y) ⊑ f x" by (rule mono) have "x ⊓ y ⊑ y" .. then show "f (x ⊓ y) ⊑ f y" by (rule mono) qed qed qed lemma join_semimorph: "(⋀x y. f x ⊔ f y ⊑ f (x ⊔ y)) ≡ (⋀x y. x ⊑ y ⟹ f x ⊑ f y)" proof assume morph: "⋀x y. f x ⊔ f y ⊑ f (x ⊔ y)" fix x y :: "'a::lattice" assume "x ⊑ y" then have "x ⊔ y = y" .. have "f x ⊑ f x ⊔ f y" .. also have "… ⊑ f (x ⊔ y)" by (rule morph) also from ‹x ⊑ y› have "x ⊔ y = y" .. finally show "f x ⊑ f y" . next assume mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y" show "⋀x y. f x ⊔ f y ⊑ f (x ⊔ y)" proof - fix x y show "f x ⊔ f y ⊑ f (x ⊔ y)" proof have "x ⊑ x ⊔ y" .. then show "f x ⊑ f (x ⊔ y)" by (rule mono) have "y ⊑ x ⊔ y" .. then show "f y ⊑ f (x ⊔ y)" by (rule mono) qed qed qed end