# Theory LOrder

Up to index of Isabelle/HOL

theory LOrder
imports Orderings
begin

    (*  Title:   HOL/LOrder.thy
        ID:      $Id: LOrder.thy,v 1.6 2005/09/20 12:03:37 wenzelm Exp $
        Author:  Steven Obua, TU Muenchen
    *)

    header {* Lattice Orders *}

    theory LOrder
    imports Orderings
    begin

    text {*
      The theory of lattices developed here is taken from the book:
      \begin{itemize}
      \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.
      \end{itemize}
    *}

    constdefs
      is_meet :: "(('a::order) => 'a => 'a) => bool"
      "is_meet m == ! a b x. m a b ≤ a ∧ m a b ≤ b ∧ (x ≤ a ∧ x ≤ b --> x ≤ m a b)"
      is_join :: "(('a::order) => 'a => 'a) => bool"
      "is_join j == ! a b x. a ≤ j a b ∧ b ≤ j a b ∧ (a ≤ x ∧ b ≤ x --> j a b ≤ x)"

    lemma is_meet_unique:
      assumes "is_meet u" "is_meet v" shows "u = v"
    proof -
      {
        fix a b :: "'a => 'a => 'a"
        assume a: "is_meet a"
        assume b: "is_meet b"
        {
          fix x y
          let ?za = "a x y"
          let ?zb = "b x y"
          from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
          with b have "?za <= ?zb" by (auto simp add: is_meet_def)
        }
      }
      note f_le = this
      show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
    qed

    lemma is_join_unique:
      assumes "is_join u" "is_join v" shows "u = v"
    proof -
      {
        fix a b :: "'a => 'a => 'a"
        assume a: "is_join a"
        assume b: "is_join b"
        {
          fix x y
          let ?za = "a x y"
          let ?zb = "b x y"
          from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
          with b have "?zb <= ?za" by (auto simp add: is_join_def)
        }
      }
      note f_le = this
      show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
    qed

    axclass join_semilorder < order
      join_exists: "? j. is_join j"

    axclass meet_semilorder < order
      meet_exists: "? m. is_meet m"

    axclass lorder < join_semilorder, meet_semilorder

    constdefs
      meet :: "('a::meet_semilorder) => 'a => 'a"
      "meet == THE m. is_meet m"
      join :: "('a::join_semilorder) => 'a => 'a"
      "join ==  THE j. is_join j"

    lemma is_meet_meet: "is_meet (meet::'a => 'a => ('a::meet_semilorder))"
    proof -
      from meet_exists obtain k::"'a => 'a => 'a" where "is_meet k" ..
      with is_meet_unique[of _ k] show ?thesis
        by (simp add: meet_def theI[of is_meet])
    qed

    lemma meet_unique: "(is_meet m) = (m = meet)"
    by (insert is_meet_meet, auto simp add: is_meet_unique)

    lemma is_join_join: "is_join (join::'a => 'a => ('a::join_semilorder))"
    proof -
      from join_exists obtain k::"'a => 'a => 'a" where "is_join k" ..
      with is_join_unique[of _ k] show ?thesis
        by (simp add: join_def theI[of is_join])
    qed

    lemma join_unique: "(is_join j) = (j = join)"
    by (insert is_join_join, auto simp add: is_join_unique)

    lemma meet_left_le: "meet a b ≤ (a::'a::meet_semilorder)"
    by (insert is_meet_meet, auto simp add: is_meet_def)

    lemma meet_right_le: "meet a b ≤ (b::'a::meet_semilorder)"
    by (insert is_meet_meet, auto simp add: is_meet_def)

    lemma meet_imp_le: "x ≤ a ==> x ≤ b ==> x ≤ meet a (b::'a::meet_semilorder)"
    by (insert is_meet_meet, auto simp add: is_meet_def)

    lemma join_left_le: "a ≤ join a (b::'a::join_semilorder)"
    by (insert is_join_join, auto simp add: is_join_def)

    lemma join_right_le: "b ≤ join a (b::'a::join_semilorder)"
    by (insert is_join_join, auto simp add: is_join_def)

    lemma join_imp_le: "a ≤ x ==> b ≤ x ==> join a b ≤ (x::'a::join_semilorder)"
    by (insert is_join_join, auto simp add: is_join_def)

    lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le

    lemma is_meet_min: "is_meet (min::'a => 'a => ('a::linorder))"
    by (auto simp add: is_meet_def min_def)

    lemma is_join_max: "is_join (max::'a => 'a => ('a::linorder))"
    by (auto simp add: is_join_def max_def)

    instance linorder ⊆ meet_semilorder
    proof
      from is_meet_min show "? (m::'a=>'a=>('a::linorder)). is_meet m" by auto
    qed

    instance linorder ⊆ join_semilorder
    proof
      from is_join_max show "? (j::'a=>'a=>('a::linorder)). is_join j" by auto
    qed

    instance linorder ⊆ lorder ..

    lemma meet_min: "meet = (min :: 'a=>'a=>('a::linorder))"
    by (simp add: is_meet_meet is_meet_min is_meet_unique)

    lemma join_max: "join = (max :: 'a=>'a=>('a::linorder))"
    by (simp add: is_join_join is_join_max is_join_unique)

    lemma meet_idempotent[simp]: "meet x x = x"
    by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)

    lemma join_idempotent[simp]: "join x x = x"
    by (rule order_antisym, simp_all add: join_left_le join_imp_le)

    lemma meet_comm: "meet x y = meet y x"
    by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)

    lemma join_comm: "join x y = join y x"
    by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)

    lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
    proof -
      have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
      hence "?l <= x & ?l <= y & ?l <= z" by auto
      hence "?l <= ?r" by (simp add: meet_imp_le)
      hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
      have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)
      hence "?r <= x & ?r <= y & ?r <= z" by (auto)
      hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
      hence b:"?r <= ?l" by (simp add: meet_imp_le)
      from a b show "?l = ?r" by auto
    qed

    lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
    proof -
      have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
      hence "x <= ?l & y <= ?l & z <= ?l" by auto
      hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
      hence a:"?r <= ?l" by (simp add: join_imp_le)
      have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
      hence "y <= ?r & z <= ?r & x <= ?r" by auto
      hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
      hence b:"?l <= ?r" by (simp add: join_imp_le)
      from a b show "?l = ?r" by auto
    qed

    lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
    by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)

    lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
    by (simp add: meet_assoc meet_comm meet_left_comm)

    lemma join_left_comm: "join a (join b c) = join b (join a c)"
    by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)

    lemma join_left_idempotent: "join y (join y x) = join y x"
    by (simp add: join_assoc join_comm join_left_comm)

    lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent

    lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent

    lemma le_def_meet: "(x <= y) = (meet x y = x)"
    proof -
      have u: "x <= y --> meet x y = x"
      proof
        assume "x <= y"
        hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
        thus "meet x y = x" by auto
      qed
      have v:"meet x y = x --> x <= y"
      proof
        have a:"meet x y <= y" by (simp add: meet_right_le)
        assume "meet x y = x"
        hence "x = meet x y" by auto
        with a show "x <= y" by (auto)
      qed
      from u v show ?thesis by blast
    qed

    lemma le_def_join: "(x <= y) = (join x y = y)"
    proof -
      have u: "x <= y --> join x y = y"
      proof
        assume "x <= y"
        hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
        thus "join x y = y" by auto
      qed
      have v:"join x y = y --> x <= y"
      proof
        have a:"x <= join x y" by (simp add: join_left_le)
        assume "join x y = y"
        hence "y = join x y" by auto
        with a show "x <= y" by (auto)
      qed
      from u v show ?thesis by blast
    qed

    lemma meet_join_absorp: "meet x (join x y) = x"
    proof -
      have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
      have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
      from a b show ?thesis by auto
    qed

    lemma join_meet_absorp: "join x (meet x y) = x"
    proof -
      have a:"x <= join x (meet x y)" by (simp add: join_left_le)
      have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
      from a b show ?thesis by auto
    qed

    lemma meet_mono: "y ≤ z ==> meet x y ≤ meet x z"
    proof -
      assume a: "y <= z"
      have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
      with a have "meet x y <= x & meet x y <= z" by auto
      thus "meet x y <= meet x z" by (simp add: meet_imp_le)
    qed

    lemma join_mono: "y ≤ z ==> join x y ≤ join x z"
    proof -
      assume a: "y ≤ z"
      have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
      with a have "x <= join x z & y <= join x z" by auto
      thus "join x y <= join x z" by (simp add: join_imp_le)
    qed

    lemma distrib_join_le: "join x (meet y z) ≤ meet (join x y) (join x z)" (is "_ <= ?r")
    proof -
      have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
      from meet_join_le have b: "meet y z <= ?r"
        by (rule_tac meet_imp_le, (blast intro: order_trans)+)
      from a b show ?thesis by (simp add: join_imp_le)
    qed

    lemma distrib_meet_le: "join (meet x y) (meet x z) ≤ meet x (join y z)" (is "?l <= _")
    proof -
      have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
      from meet_join_le have b: "?l <= join y z"
        by (rule_tac join_imp_le, (blast intro: order_trans)+)
      from a b show ?thesis by (simp add: meet_imp_le)
    qed

    lemma meet_join_eq_imp_le: "a = c ∨ a = d ∨ b = c ∨ b = d ==> meet a b ≤ join c d"
    by (insert meet_join_le, blast intro: order_trans)

    lemma modular_le: "x ≤ z ==> join x (meet y z) ≤ meet (join x y) z" (is "_ ==> ?t <= _")
    proof -
      assume a: "x <= z"
      have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
      have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
      from b c show ?thesis by (simp add: meet_imp_le)
    qed

    end

lemma is_meet_unique:

      [| is_meet u; is_meet v |] ==> u = v

lemma is_join_unique:

      [| is_join u; is_join v |] ==> u = v

lemma is_meet_meet:

      is_meet meet

lemma meet_unique:

      is_meet m = (m = meet)

lemma is_join_join:

      is_join join

lemma join_unique:

      is_join j = (j = join)

lemma meet_left_le:

      meet a b ≤ a

lemma meet_right_le:

      meet a b ≤ b

lemma meet_imp_le:

      [| x ≤ a; x ≤ b |] ==> x ≤ meet a b

lemma join_left_le:

      a ≤ join a b

lemma join_right_le:

      b ≤ join a b

lemma join_imp_le:

      [| a ≤ x; b ≤ x |] ==> join a b ≤ x

lemmas meet_join_le:

      meet a b ≤ a

      meet a b ≤ b

      a ≤ join a b

      b ≤ join a b

lemmas meet_join_le:

      meet a b ≤ a

      meet a b ≤ b

      a ≤ join a b

      b ≤ join a b

lemma is_meet_min:

      is_meet min

lemma is_join_max:

      is_join max

lemma meet_min:

      meet = min

lemma join_max:

      join = max

lemma meet_idempotent:

      meet x x = x

lemma join_idempotent:

      join x x = x

lemma meet_comm:

      meet x y = meet y x

lemma join_comm:

      join x y = join y x

lemma meet_assoc:

      meet (meet x y) z = meet x (meet y z)

lemma join_assoc:

      join (join x y) z = join x (join y z)

lemma meet_left_comm:

      meet a (meet b c) = meet b (meet a c)

lemma meet_left_idempotent:

      meet y (meet y x) = meet y x

lemma join_left_comm:

      join a (join b c) = join b (join a c)

lemma join_left_idempotent:

      join y (join y x) = join y x

lemmas meet_aci:

      meet (meet x y) z = meet x (meet y z)

      meet x y = meet y x

      meet a (meet b c) = meet b (meet a c)

      meet y (meet y x) = meet y x

lemmas meet_aci:

      meet (meet x y) z = meet x (meet y z)

      meet x y = meet y x

      meet a (meet b c) = meet b (meet a c)

      meet y (meet y x) = meet y x

lemmas join_aci:

      join (join x y) z = join x (join y z)

      join x y = join y x

      join a (join b c) = join b (join a c)

      join y (join y x) = join y x

lemmas join_aci:

      join (join x y) z = join x (join y z)

      join x y = join y x

      join a (join b c) = join b (join a c)

      join y (join y x) = join y x

lemma le_def_meet:

      (x ≤ y) = (meet x y = x)

lemma le_def_join:

      (x ≤ y) = (join x y = y)

lemma meet_join_absorp:

      meet x (join x y) = x

lemma join_meet_absorp:

      join x (meet x y) = x

lemma meet_mono:

      y ≤ z ==> meet x y ≤ meet x z

lemma join_mono:

      y ≤ z ==> join x y ≤ join x z

lemma distrib_join_le:

      join x (meet y z) ≤ meet (join x y) (join x z)

lemma distrib_meet_le:

      join (meet x y) (meet x z) ≤ meet x (join y z)

lemma meet_join_eq_imp_le:

      a = c ∨ a = d ∨ b = c ∨ b = d ==> meet a b ≤ join c d

lemma modular_le:

      x ≤ z ==> join x (meet y z) ≤ meet (join x y) z