# Theory CompleteLattice

Up to index of Isabelle/HOL/Lattice

theory CompleteLattice
imports Lattice
begin

    (*  Title:      HOL/Lattice/CompleteLattice.thy
        ID:         $Id: CompleteLattice.thy,v 1.11 2005/06/17 14:13:08 haftmann Exp $
        Author:     Markus Wenzel, TU Muenchen
    *)

    header {* 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}).
    *}

    axclass complete_lattice ⊆ partial_order
      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 \<sqsubseteq> b} sup" by blast
      hence "is_Sup A sup" by (rule Inf_Sup)
      thus ?thesis ..
    qed

    text {*
      The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
      such infimum and supremum elements.
    *}

    consts
      Meet :: "'a::complete_lattice set => 'a"
      Join :: "'a::complete_lattice set => 'a"
    syntax (xsymbols)
      Meet :: "'a::complete_lattice set => 'a"    ("\<Sqinter>_" [90] 90)
      Join :: "'a::complete_lattice set => 'a"    ("\<Squnion>_" [90] 90)
    defs
      Meet_def: "\<Sqinter>A ≡ THE inf. is_Inf A inf"
      Join_def: "\<Squnion>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 ==> \<Sqinter>A = inf"
    proof (unfold Meet_def)
      assume "is_Inf A inf"
      thus "(THE inf. is_Inf A inf) = inf"
        by (rule the_equality) (rule is_Inf_uniq)
    qed

    lemma MeetI [intro?]:
      "(!!a. a ∈ A ==> inf \<sqsubseteq> a) ==>
        (!!b. ∀a ∈ A. b \<sqsubseteq> a ==> b \<sqsubseteq> inf) ==>
        \<Sqinter>A = inf"
      by (rule Meet_equality, rule is_InfI) blast+

    lemma Join_equality [elim?]: "is_Sup A sup ==> \<Squnion>A = sup"
    proof (unfold Join_def)
      assume "is_Sup A sup"
      thus "(THE sup. is_Sup A sup) = sup"
        by (rule the_equality) (rule is_Sup_uniq)
    qed

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

    text {*
      \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
      bounds on a complete lattice structure.
    *}

    lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
    proof (unfold Meet_def)
      from ex_Inf obtain inf where "is_Inf A inf" ..
      thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
    qed

    lemma Meet_greatest [intro?]: "(!!a. a ∈ A ==> x \<sqsubseteq> a) ==> x \<sqsubseteq> \<Sqinter>A"
      by (rule is_Inf_greatest, rule is_Inf_Meet) blast

    lemma Meet_lower [intro?]: "a ∈ A ==> \<Sqinter>A \<sqsubseteq> a"
      by (rule is_Inf_lower) (rule is_Inf_Meet)

    lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
    proof (unfold Join_def)
      from ex_Sup obtain sup where "is_Sup A sup" ..
      thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
    qed

    lemma Join_least [intro?]: "(!!a. a ∈ A ==> a \<sqsubseteq> x) ==> \<Squnion>A \<sqsubseteq> x"
      by (rule is_Sup_least, rule is_Sup_Join) blast
    lemma Join_lower [intro?]: "a ∈ A ==> a \<sqsubseteq> \<Squnion>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:
      "(!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y) ==> ∃a::'a::complete_lattice. f a = a"
    proof
      assume mono: "!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y"
      let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
      have ge: "f ?a \<sqsubseteq> ?a"
      proof
        fix x assume x: "x ∈ ?H"
        hence "?a \<sqsubseteq> x" ..
        hence "f ?a \<sqsubseteq> f x" by (rule mono)
        also from x have "... \<sqsubseteq> x" ..
        finally show "f ?a \<sqsubseteq> x" .
      qed
      also have "?a \<sqsubseteq> f ?a"
      proof
        from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
        thus "f ?a ∈ ?H" ..
      qed
      finally show "f ?a = ?a" .
    qed

    subsection {* Bottom and top elements *}

    text {*
      With general bounds available, complete lattices also have least and
      greatest elements.
    *}

    constdefs
      bottom :: "'a::complete_lattice"    ("⊥")
      "⊥ ≡ \<Sqinter>UNIV"
      top :: "'a::complete_lattice"    ("\<top>")
      "\<top> ≡ \<Squnion>UNIV"

    lemma bottom_least [intro?]: "⊥ \<sqsubseteq> x"
    proof (unfold bottom_def)
      have "x ∈ UNIV" ..
      thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
    qed

    lemma bottomI [intro?]: "(!!a. x \<sqsubseteq> a) ==> ⊥ = x"
    proof (unfold bottom_def)
      assume "!!a. x \<sqsubseteq> a"
      show "\<Sqinter>UNIV = x"
      proof
        fix a show "x \<sqsubseteq> a" .
      next
        fix b :: "'a::complete_lattice"
        assume b: "∀a ∈ UNIV. b \<sqsubseteq> a"
        have "x ∈ UNIV" ..
        with b show "b \<sqsubseteq> x" ..
      qed
    qed

    lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
    proof (unfold top_def)
      have "x ∈ UNIV" ..
      thus "x \<sqsubseteq> \<Squnion>UNIV" ..
    qed

    lemma topI [intro?]: "(!!a. a \<sqsubseteq> x) ==> \<top> = x"
    proof (unfold top_def)
      assume "!!a. a \<sqsubseteq> x"
      show "\<Squnion>UNIV = x"
      proof
        fix a show "a \<sqsubseteq> x" .
      next
        fix b :: "'a::complete_lattice"
        assume b: "∀a ∈ UNIV. a \<sqsubseteq> b"
        have "x ∈ UNIV" ..
        with b show "x \<sqsubseteq> 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)
        hence "∃sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
        thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
      qed
    qed

    text {*
      Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
      other.
    *}

    theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
    proof -
      from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
      hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
      thus ?thesis ..
    qed

    theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
    proof -
      from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
      hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
      thus ?thesis ..
    qed

    text {*
      Likewise are @{text ⊥} and @{text \<top>} duals of each other.
    *}

    theorem dual_bottom [intro?]: "dual ⊥ = \<top>"
    proof -
      have "\<top> = dual ⊥"
      proof
        fix a' have "⊥ \<sqsubseteq> undual a'" ..
        hence "dual (undual a') \<sqsubseteq> dual ⊥" ..
        thus "a' \<sqsubseteq> dual ⊥" by simp
      qed
      thus ?thesis ..
    qed

    theorem dual_top [intro?]: "dual \<top> = ⊥"
    proof -
      have "⊥ = dual \<top>"
      proof
        fix a' have "undual a' \<sqsubseteq> \<top>" ..
        hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
        thus "dual \<top> \<sqsubseteq> a'" by simp
      qed
      thus ?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 (\<Sqinter>{x, y})"
    proof -
      have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
      thus ?thesis by (simp only: is_Inf_binary)
    qed

    lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
    proof -
      have "is_Sup {x, y} (\<Squnion>{x, y})" ..
      thus ?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 \<sqinter> y = \<Sqinter>{x, y}"
      by (rule meet_equality) (rule is_inf_binary)

    theorem join_binary: "x \<squnion> y = \<Squnion>{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 ==> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
    proof (rule Meet_greatest)
      fix a assume "a ∈ A"
      also assume "A ⊆ B"
      finally have "a ∈ B" .
      thus "\<Sqinter>B \<sqsubseteq> a" ..
    qed

    theorem Join_subset_mono: "A ⊆ B ==> \<Squnion>A \<sqsubseteq> \<Squnion>B"
    proof -
      assume "A ⊆ B"
      hence "dual ` A ⊆ dual ` B" by blast
      hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
      hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
      thus ?thesis by (simp only: dual_leq)
    qed

    text {*
      Bounds over unions of sets may be obtained separately.
    *}

    theorem Meet_Un: "\<Sqinter>(A ∪ B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
    proof
      fix a assume "a ∈ A ∪ B"
      thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
      proof
        assume a: "a ∈ A"
        have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
        also from a have "… \<sqsubseteq> a" ..
        finally show ?thesis .
      next
        assume a: "a ∈ B"
        have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
        also from a have "… \<sqsubseteq> a" ..
        finally show ?thesis .
      qed
    next
      fix b assume b: "∀a ∈ A ∪ B. b \<sqsubseteq> a"
      show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
      proof
        show "b \<sqsubseteq> \<Sqinter>A"
        proof
          fix a assume "a ∈ A"
          hence "a ∈  A ∪ B" ..
          with b show "b \<sqsubseteq> a" ..
        qed
        show "b \<sqsubseteq> \<Sqinter>B"
        proof
          fix a assume "a ∈ B"
          hence "a ∈  A ∪ B" ..
          with b show "b \<sqsubseteq> a" ..
        qed
      qed
    qed

    theorem Join_Un: "\<Squnion>(A ∪ B) = \<Squnion>A \<squnion> \<Squnion>B"
    proof -
      have "dual (\<Squnion>(A ∪ B)) = \<Sqinter>(dual ` A ∪ dual ` B)"
        by (simp only: dual_Join image_Un)
      also have "… = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)"
        by (rule Meet_Un)
      also have "… = dual (\<Squnion>A \<squnion> \<Squnion>B)"
        by (simp only: dual_join dual_Join)
      finally show ?thesis ..
    qed

    text {*
      Bounds over singleton sets are trivial.
    *}

    theorem Meet_singleton: "\<Sqinter>{x} = x"
    proof
      fix a assume "a ∈ {x}"
      hence "a = x" by simp
      thus "x \<sqsubseteq> a" by (simp only: leq_refl)
    next
      fix b assume "∀a ∈ {x}. b \<sqsubseteq> a"
      thus "b \<sqsubseteq> x" by simp
    qed

    theorem Join_singleton: "\<Squnion>{x} = x"
    proof -
      have "dual (\<Squnion>{x}) = \<Sqinter>{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: "\<Sqinter>{} = \<Squnion>UNIV"
    proof
      fix a :: "'a::complete_lattice"
      assume "a ∈ {}"
      hence False by simp
      thus "\<Squnion>UNIV \<sqsubseteq> a" ..
    next
      fix b :: "'a::complete_lattice"
      have "b ∈ UNIV" ..
      thus "b \<sqsubseteq> \<Squnion>UNIV" ..
    qed

    theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
    proof -
      have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
      also have "… = \<Squnion>UNIV" by (rule Meet_empty)
      also have "… = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
      finally show ?thesis ..
    qed

    end

### Complete lattice operations

theorem ex_Sup:

      ∃sup. is_Sup A sup

lemma Meet_equality:

      is_Inf A inf ==> Meet A = inf

lemma MeetI:

      [| !!a. a ∈ A ==> inf [= a; !!b. ∀a∈A. b [= a ==> b [= inf |] ==> Meet A = inf

lemma Join_equality:

      is_Sup A sup ==> Join A = sup

lemma JoinI:

      [| !!a. a ∈ A ==> a [= sup; !!b. ∀a∈A. a [= b ==> sup [= b |] ==> Join A = sup

lemma is_Inf_Meet:

      is_Inf A (Meet A)

lemma Meet_greatest:

      (!!a. a ∈ A ==> x [= a) ==> x [= Meet A

lemma Meet_lower:

      a ∈ A ==> Meet A [= a

lemma is_Sup_Join:

      is_Sup A (Join A)

lemma Join_least:

      (!!a. a ∈ A ==> a [= x) ==> Join A [= x

lemma Join_lower:

      a ∈ A ==> a [= Join A

### The Knaster-Tarski Theorem

theorem Knaster_Tarski:

      (!!x y. x [= y ==> f x [= f y) ==> ∃a. f a = a

### Bottom and top elements

lemma bottom_least:

      ⊥ [= x

lemma bottomI:

      (!!a. x [= a) ==> ⊥ = x

lemma top_greatest:

      x [= \<top>

lemma topI:

      (!!a. a [= x) ==> \<top> = x

### Duality

theorem dual_Meet:

      dual (Meet A) = Join (dual ` A)

theorem dual_Join:

      dual (Join A) = Meet (dual ` A)

theorem dual_bottom:

      dual ⊥ = \<top>

theorem dual_top:

      dual \<top> = ⊥

### Complete lattices are lattices

lemma is_inf_binary:

      is_inf x y (Meet {x, y})

lemma is_sup_binary:

      is_sup x y (Join {x, y})

theorem meet_binary:

      Lattice.meet x y = Meet {x, y}

theorem join_binary:

      Lattice.join x y = Join {x, y}

### Complete lattices and set-theory operations

theorem Meet_subset_antimono:

      A ⊆ B ==> Meet B [= Meet A

theorem Join_subset_mono:

      A ⊆ B ==> Join A [= Join B

theorem Meet_Un:

      Meet (A ∪ B) = Lattice.meet (Meet A) (Meet B)

theorem Join_Un:

      Join (A ∪ B) = Lattice.join (Join A) (Join B)

theorem Meet_singleton:

      Meet {x} = x

theorem Join_singleton:

      Join {x} = x

theorem Meet_empty:

      Meet {} = Join UNIV

theorem Join_empty:

      Join {} = Meet UNIV