Quelle  CompleteLattice.thy

(*  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 🍋‹‹pages 93--94› in "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