Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lattice.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Lattices\<close>

theory Lattice imports Bounds begin

subsection \<open>Lattice operations\<close>

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

class lattice =
  assumes ex_inf: "\inf. is_inf x y inf"
  assumes ex_sup: "\sup. is_sup x y sup"

text \<open>
  The \<open>\<sqinter>\<close> (meet) and \<open>\<squnion>\<close> (join) operations select such
  infimum and supremum elements.
\<close>

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

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 _ \<open>is_inf x y inf\<close>])
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 _ \<open>is_sup x y sup\<close>])
qed

lemma joinI [intro?]: "x \ sup \ y \ sup \
    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = 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 lattice structure.
\<close>

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 _ \<open>is_inf x y inf\<close>])
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 _ \<open>is_sup x y sup\<close>])
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 \<open>Duality\<close>

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

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

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 \<open>Algebraic properties \label{sec:lattice-algebra}\<close>

text \<open>
  The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations have the following
  characteristic algebraic properties: associative (A), commutative
  (C), and absorptive (AB).
\<close>

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 \<open>
  \medskip Some further algebraic properties hold as well.  The
  property idempotent (I) is a basic algebraic consequence of (AB).
\<close>

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 \<open>
  Meet and join are trivial for related elements.
\<close>

theorem meet_related [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 join_related [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 \<open>Order versus algebraic structure\<close>

text \<open>
  The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are connected with the
  underlying \<open>\<sqsubseteq>\<close> relation in a canonical manner.
\<close>

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 \<open>
  \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 \<open>\<sqinter>\<close> and \<open>\<squnion>\<close>
  such that (A), (C), and (AB) hold (cf.\
  \S\ref{sec:lattice-algebra}).  This structure represents a lattice,
  if the relation \<^term>\<open>x \<sqsubseteq> y\<close> is defined as \<^term>\<open>x \<sqinter> y = x\<close>
  (alternatively as \<^term>\<open>x \<squnion> y = y\<close>).  Furthermore, infimum and
  supremum with respect to this ordering coincide with the original
  \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations.
\<close>

subsection \<open>Example instances\<close>

subsubsection \<open>Linear orders\<close>

text \<open>
  Linear orders with \<^term>\<open>minimum\<close> and \<^term>\<open>maximum\<close> operations
  are a (degenerate) example of lattice structures.
\<close>

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 \<subseteq> 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 \<open>
  The lattice operations on linear orders indeed coincide with \<^term>\<open>minimum\<close> and \<^term>\<open>maximum\<close>.
\<close>

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 \<open>Binary products\<close>

text \<open>
  The class of lattices is closed under direct binary products (cf.\
  \S\ref{sec:prod-order}).
\<close>

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 \<open>
  The lattice operations on a binary product structure indeed coincide
  with the products of the original ones.
\<close>

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 \<open>General products\<close>

text \<open>
  The class of lattices is closed under general products (function
  spaces) as well (cf.\ \S\ref{sec:fun-order}).
\<close>

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 \<open>
  The lattice operations on a general product structure (function
  space) indeed emerge by point-wise lifting of the original ones.
\<close>

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 \<open>Monotonicity and semi-morphisms\<close>

text \<open>
  The lattice operations are monotone in both argument positions.  In
  fact, monotonicity of the second position is trivial due to
  commutativity.
\<close>

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 \<open>
  \medskip A semi-morphisms is a function \<open>f\<close> that preserves the
  lattice operations in the following manner: \<^term>\<open>f (x \<sqinter> y) \<sqsubseteq> f x
  \<sqinter> f y\<close> and \<^term>\<open>f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)\<close>, respectively.  Any of
  these properties is equivalent with monotonicity.
\<close>

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 \<open>x \<sqsubseteq> y\<close> have "x \<squnion> 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

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.