Quelle CompleteLattice.thy Sprache: Isabelle

(*  Title:      HOL/Lattice/CompleteLattice.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section \<open>Complete lattices\<close>

theory CompleteLattice imports Lattice begin

subsection \<open>Complete lattice operations\<close>

text \<open>
  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}).
\<close>

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 \<open>
  The general \<open>\<Sqinter>\<close> (meet) and \<open>\<Squnion>\<close> (join) operations select
  such infimum and supremum elements.
\<close>

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 \<open>
  Due to unique existence of bounds, the complete lattice operations
  may be exhibited as follows.
\<close>

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 _ \<open>is_Inf A inf\<close>])
qed

lemma MeetI [intro?]:
  "(\a. a \ A \ inf \ a) \
    (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>
    \<Sqinter>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 _ \<open>is_Sup A sup\<close>])
qed

lemma JoinI [intro?]:
  "(\a. a \ A \ a \ sup) \
    (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>
    \<Squnion>A = sup"
  by (rule Join_equality, rule is_SupI) blast+

text \<open>
  \medskip The \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations indeed determine
  bounds on a complete lattice structure.
\<close>

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 _ \<open>is_Inf A inf\<close>])
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 _ \<open>is_Sup A sup\<close>])
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 \<open>The Knaster-Tarski Theorem\<close>

text \<open>
  The Knaster-Tarski Theorem (in its simplest formulation) states that
  any monotone function on a complete lattice has a least fixed-point
  (see \<^cite>\<open>\<open>pages 93--94\<close> in "Davey-Priestley:1990"\<close> for example).  This
  is a consequence of the basic boundary properties of the complete
  lattice operations.
\<close>

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 \<open>Bottom and top elements\<close>

text \<open>
  With general bounds available, complete lattices also have least and
  greatest elements.
\<close>

definition
  bottom :: "'a::complete_lattice"  (\<open>\<bottom>\<close>) where
  "\ = \UNIV"

definition
  top :: "'a::complete_lattice"  (\<open>\<top>\<close>) 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 \<open>Duality\<close>

text \<open>
  The class of complete lattices is closed under formation of dual
  structures.
\<close>

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 \<open>
  Apparently, the \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations are dual to each
  other.
\<close>

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 \<open>
  Likewise are \<open>\<bottom>\<close> and \<open>\<top>\<close> duals of each other.
\<close>

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' \<sqsubseteq> \<top>" ..
    then have "dual \ \ dual (undual a')" ..
    then show "dual \ \ a'" by simp
  qed
  then show ?thesis ..
qed

subsection \<open>Complete lattices are lattices\<close>

text \<open>
  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}.
\<close>

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 \<subseteq> 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 \<open>Complete lattices and set-theory operations\<close>

text \<open>
  The complete lattice operations are (anti) monotone wrt.\ set
  inclusion.
\<close>

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 \<open>
  Bounds over unions of sets may be obtained separately.
\<close>

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 \<open>
  Bounds over singleton sets are trivial.
\<close>

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 \<open>
  Bounds over the empty and universal set correspond to each other.
\<close>

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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.