Quelle  Lattice.thy   Sprache: Isabelle

(*  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 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 ‹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.java.lang.NullPointerException
  \S\ref{sec:lattice-algebra}).  This structure represents a lattice,
  if the relation 🍋‹x ⊑ y› is defined as 🍋‹x ⊓ y = x›
  (alternatively as 🍋‹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 🍋‹minimum› and 🍋‹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 🍋‹minimum› and 🍋‹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.java.lang.NullPointerException
  \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 \<dots> show \<dots> .."} 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: 🍋‹f (x ⊓ y) ⊑ f x
  ⊓ f y› and 🍋‹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