(* Title: HOL/Lattice/CompleteLattice.thy Author: Markus Wenzel, TU Muenchen *) section ‹Complete lattices› theory CompleteLattice imports Lattice begin 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}). › class complete_lattice = assumes 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 then have "is_Sup A sup" by (rule Inf_Sup) then show ?thesis .. qed text ‹ The general ‹⨅› (meet) and ‹⨆› (join) operations select such infimum and supremum elements. › definition Meet :: "'a::complete_lattice set ⇒ 'a" ("⨅_" [90] 90) where "⨅A = (THE inf. is_Inf A inf)" definition Join :: "'a::complete_lattice set ⇒ 'a" ("⨆_" [90] 90) where "⨆A = (THE 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" then show "(THE inf. is_Inf A inf) = inf" by (rule the_equality) (rule is_Inf_uniq [OF _ ‹is_Inf A inf›]) 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" then show "(THE sup. is_Sup A sup) = sup" by (rule the_equality) (rule is_Sup_uniq [OF _ ‹is_Sup A sup›]) 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 ‹⨅› 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›]) 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 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›]) 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: assumes mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y" obtains a :: "'a::complete_lattice" where "f a = a" and "⋀a'. f a' = a' ⟹ a ⊑ a'" proof let ?H = "{u. f u ⊑ u}" let ?a = "⨅?H" show "f ?a = ?a" proof - have ge: "f ?a ⊑ ?a" proof fix x assume x: "x ∈ ?H" then have "?a ⊑ x" .. then have "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) then show "f ?a ∈ ?H" .. qed finally show ?thesis . qed fix a' assume "f a' = a'" then have "f a' ⊑ a'" by (simp only: leq_refl) then have "a' ∈ ?H" .. then show "?a ⊑ a'" .. qed theorem Knaster_Tarski_dual: assumes mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y" obtains a :: "'a::complete_lattice" where "f a = a" and "⋀a'. f a' = a' ⟹ a' ⊑ a" proof let ?H = "{u. u ⊑ f u}" let ?a = "⨆?H" show "f ?a = ?a" proof - have le: "?a ⊑ f ?a" proof fix x assume x: "x ∈ ?H" then have "x ⊑ f x" .. also from x have "x ⊑ ?a" .. then have "f x ⊑ f ?a" by (rule mono) finally show "x ⊑ f ?a" . qed have "f ?a ⊑ ?a" proof from le have "f ?a ⊑ f (f ?a)" by (rule mono) then show "f ?a ∈ ?H" .. qed from this and le show ?thesis by (rule leq_antisym) qed fix a' assume "f a' = a'" then have "a' ⊑ f a'" by (simp only: leq_refl) then have "a' ∈ ?H" .. then show "a' ⊑ ?a" .. qed subsection ‹Bottom and top elements› text ‹ With general bounds available, complete lattices also have least and greatest elements. › definition bottom :: "'a::complete_lattice" ("⊥") where "⊥ = ⨅UNIV" definition top :: "'a::complete_lattice" ("⊤") where "⊤ = ⨆UNIV" lemma bottom_least [intro?]: "⊥ ⊑ x" proof (unfold bottom_def) have "x ∈ UNIV" .. then show "⨅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" by fact 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" .. then show "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" by fact 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 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) then have "∃sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf) then show ?thesis by (simp add: dual_ex [symmetric] image_comp) qed qed text ‹ Apparently, the ‹⨅› and ‹⨆› 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))" .. then have "⨆(dual ` A) = dual (⨅A)" .. then show ?thesis .. qed theorem dual_Join [intro?]: "dual (⨆A) = ⨅(dual ` A)" proof - from is_Sup_Join have "is_Inf (dual ` A) (dual (⨆A))" .. then have "⨅(dual ` A) = dual (⨆A)" .. then show ?thesis .. qed text ‹ Likewise are ‹⊥› and ‹⊤› duals of each other. › theorem dual_bottom [intro?]: "dual ⊥ = ⊤" proof - have "⊤ = dual ⊥" proof fix a' have "⊥ ⊑ undual a'" .. then have "dual (undual a') ⊑ dual ⊥" .. then show "a' ⊑ dual ⊥" by simp qed then show ?thesis .. qed theorem dual_top [intro?]: "dual ⊤ = ⊥" proof - have "⊥ = dual ⊤" proof fix a' have "undual a' ⊑ ⊤" .. then have "dual ⊤ ⊑ dual (undual a')" .. then show "dual ⊤ ⊑ a'" by simp qed then show ?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 (⨅{x, y})" proof - have "is_Inf {x, y} (⨅{x, y})" .. then show ?thesis by (simp only: is_Inf_binary) qed lemma is_sup_binary: "is_sup x y (⨆{x, y})" proof - have "is_Sup {x, y} (⨆{x, y})" .. then show ?thesis by (simp only: is_Sup_binary) qed instance complete_lattice ⊆ lattice proof fix x y :: "'a::complete_lattice" from is_inf_binary show "∃inf. is_inf x y inf" .. from is_sup_binary show "∃sup. is_sup x y sup" .. qed theorem meet_binary: "x ⊓ y = ⨅{x, y}" by (rule meet_equality) (rule is_inf_binary) theorem join_binary: "x ⊔ y = ⨆{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 ⊆ B ⟹ ⨅B ⊑ ⨅A" proof (rule Meet_greatest) fix a assume "a ∈ A" also assume "A ⊆ B" finally have "a ∈ B" . then show "⨅B ⊑ a" .. qed theorem Join_subset_mono: "A ⊆ B ⟹ ⨆A ⊑ ⨆B" proof - assume "A ⊆ B" then have "dual ` A ⊆ dual ` B" by blast then have "⨅(dual ` B) ⊑ ⨅(dual ` A)" by (rule Meet_subset_antimono) then have "dual (⨆B) ⊑ dual (⨆A)" by (simp only: dual_Join) then show ?thesis by (simp only: dual_leq) qed text ‹ Bounds over unions of sets may be obtained separately. › theorem Meet_Un: "⨅(A ∪ B) = ⨅A ⊓ ⨅B" proof fix a assume "a ∈ A ∪ B" then show "⨅A ⊓ ⨅B ⊑ a" proof assume a: "a ∈ A" have "⨅A ⊓ ⨅B ⊑ ⨅A" .. also from a have "… ⊑ a" .. finally show ?thesis . next assume a: "a ∈ B" have "⨅A ⊓ ⨅B ⊑ ⨅B" .. also from a have "… ⊑ a" .. finally show ?thesis . qed next fix b assume b: "∀a ∈ A ∪ B. b ⊑ a" show "b ⊑ ⨅A ⊓ ⨅B" proof show "b ⊑ ⨅A" proof fix a assume "a ∈ A" then have "a ∈ A ∪ B" .. with b show "b ⊑ a" .. qed show "b ⊑ ⨅B" proof fix a assume "a ∈ B" then have "a ∈ A ∪ B" .. with b show "b ⊑ a" .. qed qed qed theorem Join_Un: "⨆(A ∪ B) = ⨆A ⊔ ⨆B" proof - have "dual (⨆(A ∪ B)) = ⨅(dual ` A ∪ dual ` B)" by (simp only: dual_Join image_Un) also have "… = ⨅(dual ` A) ⊓ ⨅(dual ` B)" by (rule Meet_Un) also have "… = dual (⨆A ⊔ ⨆B)" by (simp only: dual_join dual_Join) finally show ?thesis .. qed text ‹ Bounds over singleton sets are trivial. › theorem Meet_singleton: "⨅{x} = x" proof fix a assume "a ∈ {x}" then have "a = x" by simp then show "x ⊑ a" by (simp only: leq_refl) next fix b assume "∀a ∈ {x}. b ⊑ a" then show "b ⊑ x" by simp qed theorem Join_singleton: "⨆{x} = x" proof - have "dual (⨆{x}) = ⨅{dual x}" by (simp add: dual_Join) also have "… = 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: "⨅{} = ⨆UNIV" proof fix a :: "'a::complete_lattice" assume "a ∈ {}" then have False by simp then show "⨆UNIV ⊑ a" .. next fix b :: "'a::complete_lattice" have "b ∈ UNIV" .. then show "b ⊑ ⨆UNIV" .. qed theorem Join_empty: "⨆{} = ⨅UNIV" proof - have "dual (⨆{}) = ⨅{}" by (simp add: dual_Join) also have "… = ⨆UNIV" by (rule Meet_empty) also have "… = dual (⨅UNIV)" by (simp add: dual_Meet) finally show ?thesis .. qed end