Theory HOL.Lattices

(*  Title:      HOL/Lattices.thy
    Author:     Tobias Nipkow
*)

section ‹Abstract lattices›

theory Lattices
imports Groups
begin

subsection ‹Abstract semilattice›

text ‹
  These locales provide a basic structure for interpretation into
  bigger structures;  extensions require careful thinking, otherwise
  undesired effects may occur due to interpretation.
›

locale semilattice = abel_semigroup +
  assumes idem [simp]: "a ❙* a = a"
begin

lemma left_idem [simp]: "a ❙* (a ❙* b) = a ❙* b"
  by (simp add: assoc [symmetric])

lemma right_idem [simp]: "(a ❙* b) ❙* b = a ❙* b"
  by (simp add: assoc)

end

locale semilattice_neutr = semilattice + comm_monoid

locale semilattice_order = semilattice +
  fixes less_eq :: "'a ⇒ 'a ⇒ bool"  (infix ‹❙≤› 50)
    and less :: "'a ⇒ 'a ⇒ bool"  (infix ‹❙<› 50)
  assumes order_iff: "a ❙≤ b ⟷ a = a ❙* b"
    and strict_order_iff: "a ❙< b ⟷ a = a ❙* b ∧ a ≠ b"
begin

lemma orderI: "a = a ❙* b ⟹ a ❙≤ b"
  by (simp add: order_iff)

lemma orderE:
  assumes "a ❙≤ b"
  obtains "a = a ❙* b"
  using assms by (unfold order_iff)

sublocale ordering less_eq less
proof
  show "a ❙< b ⟷ a ❙≤ b ∧ a ≠ b" for a b
    by (simp add: order_iff strict_order_iff)
next
  show "a ❙≤ a" for a
    by (simp add: order_iff)
next
  fix a b
  assume "a ❙≤ b" "b ❙≤ a"
  then have "a = a ❙* b" "a ❙* b = b"
    by (simp_all add: order_iff commute)
  then show "a = b" by simp
next
  fix a b c
  assume "a ❙≤ b" "b ❙≤ c"
  then have "a = a ❙* b" "b = b ❙* c"
    by (simp_all add: order_iff commute)
  then have "a = a ❙* (b ❙* c)"
    by simp
  then have "a = (a ❙* b) ❙* c"
    by (simp add: assoc)
  with ‹a = a ❙* b› [symmetric] have "a = a ❙* c" by simp
  then show "a ❙≤ c" by (rule orderI)
qed

lemma cobounded1 [simp]: "a ❙* b ❙≤ a"
  by (simp add: order_iff commute)

lemma cobounded2 [simp]: "a ❙* b ❙≤ b"
  by (simp add: order_iff)

lemma boundedI:
  assumes "a ❙≤ b" and "a ❙≤ c"
  shows "a ❙≤ b ❙* c"
proof (rule orderI)
  from assms obtain "a ❙* b = a" and "a ❙* c = a"
    by (auto elim!: orderE)
  then show "a = a ❙* (b ❙* c)"
    by (simp add: assoc [symmetric])
qed

lemma boundedE:
  assumes "a ❙≤ b ❙* c"
  obtains "a ❙≤ b" and "a ❙≤ c"
  using assms by (blast intro: trans cobounded1 cobounded2)

lemma bounded_iff [simp]: "a ❙≤ b ❙* c ⟷ a ❙≤ b ∧ a ❙≤ c"
  by (blast intro: boundedI elim: boundedE)

lemma strict_boundedE:
  assumes "a ❙< b ❙* c"
  obtains "a ❙< b" and "a ❙< c"
  using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+

lemma coboundedI1: "a ❙≤ c ⟹ a ❙* b ❙≤ c"
  by (rule trans) auto

lemma coboundedI2: "b ❙≤ c ⟹ a ❙* b ❙≤ c"
  by (rule trans) auto

lemma strict_coboundedI1: "a ❙< c ⟹ a ❙* b ❙< c"
  using irrefl
  by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order
      elim: strict_boundedE)

lemma strict_coboundedI2: "b ❙< c ⟹ a ❙* b ❙< c"
  using strict_coboundedI1 [of b c a] by (simp add: commute)

lemma mono: "a ❙≤ c ⟹ b ❙≤ d ⟹ a ❙* b ❙≤ c ❙* d"
  by (blast intro: boundedI coboundedI1 coboundedI2)

lemma absorb1: "a ❙≤ b ⟹ a ❙* b = a"
  by (rule antisym) (auto simp: refl)

lemma absorb2: "b ❙≤ a ⟹ a ❙* b = b"
  by (rule antisym) (auto simp: refl)

lemma absorb3: "a ❙< b ⟹ a ❙* b = a"
  by (rule absorb1) (rule strict_implies_order)

lemma absorb4: "b ❙< a ⟹ a ❙* b = b"
  by (rule absorb2) (rule strict_implies_order)

lemma absorb_iff1: "a ❙≤ b ⟷ a ❙* b = a"
  using order_iff by auto

lemma absorb_iff2: "b ❙≤ a ⟷ a ❙* b = b"
  using order_iff by (auto simp add: commute)

end

locale semilattice_neutr_order = semilattice_neutr + semilattice_order
begin

sublocale ordering_top less_eq less "❙1"
  by standard (simp add: order_iff)

lemma eq_neutr_iff [simp]: ‹a ❙* b = ❙1 ⟷ a = ❙1 ∧ b = ❙1›
  by (simp add: eq_iff)

lemma neutr_eq_iff [simp]: ‹❙1 = a ❙* b ⟷ a = ❙1 ∧ b = ❙1›
  by (simp add: eq_iff)

end

text ‹Interpretations for boolean operators›

interpretation conj: semilattice_neutr ‹(∧)› True
  by standard auto

interpretation disj: semilattice_neutr ‹(∨)› False
  by standard auto

declare conj_assoc [ac_simps del] disj_assoc [ac_simps del] ― ‹already simp by default›


subsection ‹Syntactic infimum and supremum operations›

class inf =
  fixes inf :: "'a ⇒ 'a ⇒ 'a" (infixl ‹⊓› 70)

class sup =
  fixes sup :: "'a ⇒ 'a ⇒ 'a" (infixl ‹⊔› 65)


subsection ‹Concrete lattices›

class semilattice_inf = order + inf +
  assumes inf_le1 [simp]: "x ⊓ y ≤ x"
  and inf_le2 [simp]: "x ⊓ y ≤ y"
  and inf_greatest: "x ≤ y ⟹ x ≤ z ⟹ x ≤ y ⊓ z"

class semilattice_sup = order + sup +
  assumes sup_ge1 [simp]: "x ≤ x ⊔ y"
  and sup_ge2 [simp]: "y ≤ x ⊔ y"
  and sup_least: "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
begin

text ‹Dual lattice.›
lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater"
  by (rule class.semilattice_inf.intro, rule dual_order)
    (unfold_locales, simp_all add: sup_least)

end

class lattice = semilattice_inf + semilattice_sup


subsubsection ‹Intro and elim rules›

context semilattice_inf
begin

lemma le_infI1: "a ≤ x ⟹ a ⊓ b ≤ x"
  by (rule order_trans) auto

lemma le_infI2: "b ≤ x ⟹ a ⊓ b ≤ x"
  by (rule order_trans) auto

lemma le_infI: "x ≤ a ⟹ x ≤ b ⟹ x ≤ a ⊓ b"
  by (fact inf_greatest) (* FIXME: duplicate lemma *)

lemma le_infE: "x ≤ a ⊓ b ⟹ (x ≤ a ⟹ x ≤ b ⟹ P) ⟹ P"
  by (blast intro: order_trans inf_le1 inf_le2)

lemma le_inf_iff: "x ≤ y ⊓ z ⟷ x ≤ y ∧ x ≤ z"
  by (blast intro: le_infI elim: le_infE) (* [simp] via bounded_iff *)

lemma le_iff_inf: "x ≤ y ⟷ x ⊓ y = x"
  by (auto intro: le_infI1 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_inf_iff)

lemma inf_mono: "a ≤ c ⟹ b ≤ d ⟹ a ⊓ b ≤ c ⊓ d"
  by (fast intro: inf_greatest le_infI1 le_infI2)

end

context semilattice_sup
begin

lemma le_supI1: "x ≤ a ⟹ x ≤ a ⊔ b"
  by (rule order_trans) auto

lemma le_supI2: "x ≤ b ⟹ x ≤ a ⊔ b"
  by (rule order_trans) auto

lemma le_supI: "a ≤ x ⟹ b ≤ x ⟹ a ⊔ b ≤ x"
  by (fact sup_least) (* FIXME: duplicate lemma *)

lemma le_supE: "a ⊔ b ≤ x ⟹ (a ≤ x ⟹ b ≤ x ⟹ P) ⟹ P"
  by (blast intro: order_trans sup_ge1 sup_ge2)

lemma le_sup_iff: "x ⊔ y ≤ z ⟷ x ≤ z ∧ y ≤ z"
  by (blast intro: le_supI elim: le_supE) (* [simp] via bounded_iff *)

lemma le_iff_sup: "x ≤ y ⟷ x ⊔ y = y"
  by (auto intro: le_supI2 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_sup_iff)

lemma sup_mono: "a ≤ c ⟹ b ≤ d ⟹ a ⊔ b ≤ c ⊔ d"
  by (fast intro: sup_least le_supI1 le_supI2)

end


subsubsection ‹Equational laws›

context semilattice_inf
begin

sublocale inf: semilattice inf
proof
  fix a b c
  show "(a ⊓ b) ⊓ c = a ⊓ (b ⊓ c)"
    by (rule order.antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
  show "a ⊓ b = b ⊓ a"
    by (rule order.antisym) (auto simp add: le_inf_iff)
  show "a ⊓ a = a"
    by (rule order.antisym) (auto simp add: le_inf_iff)
qed

sublocale inf: semilattice_order inf less_eq less
  by standard (auto simp add: le_iff_inf less_le)

lemma inf_assoc: "(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)"
  by (fact inf.assoc)

lemma inf_commute: "(x ⊓ y) = (y ⊓ x)"
  by (fact inf.commute)

lemma inf_left_commute: "x ⊓ (y ⊓ z) = y ⊓ (x ⊓ z)"
  by (fact inf.left_commute)

lemma inf_idem: "x ⊓ x = x"
  by (fact inf.idem) (* already simp *)

lemma inf_left_idem: "x ⊓ (x ⊓ y) = x ⊓ y"
  by (fact inf.left_idem) (* already simp *)

lemma inf_right_idem: "(x ⊓ y) ⊓ y = x ⊓ y"
  by (fact inf.right_idem) (* already simp *)

lemma inf_absorb1: "x ≤ y ⟹ x ⊓ y = x"
  by (rule order.antisym) auto

lemma inf_absorb2: "y ≤ x ⟹ x ⊓ y = y"
  by (rule order.antisym) auto

lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem

end

context semilattice_sup
begin

sublocale sup: semilattice sup
proof
  fix a b c
  show "(a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)"
    by (rule order.antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
  show "a ⊔ b = b ⊔ a"
    by (rule order.antisym) (auto simp add: le_sup_iff)
  show "a ⊔ a = a"
    by (rule order.antisym) (auto simp add: le_sup_iff)
qed

sublocale sup: semilattice_order sup greater_eq greater
  by standard (auto simp add: le_iff_sup sup.commute less_le)

lemma sup_assoc: "(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
  by (fact sup.assoc)

lemma sup_commute: "(x ⊔ y) = (y ⊔ x)"
  by (fact sup.commute)

lemma sup_left_commute: "x ⊔ (y ⊔ z) = y ⊔ (x ⊔ z)"
  by (fact sup.left_commute)

lemma sup_idem: "x ⊔ x = x"
  by (fact sup.idem) (* already simp *)

lemma sup_left_idem [simp]: "x ⊔ (x ⊔ y) = x ⊔ y"
  by (fact sup.left_idem)

lemma sup_absorb1: "y ≤ x ⟹ x ⊔ y = x"
  by (rule order.antisym) auto

lemma sup_absorb2: "x ≤ y ⟹ x ⊔ y = y"
  by (rule order.antisym) auto

lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem

end

context lattice
begin

lemma dual_lattice: "class.lattice sup (≥) (>) inf"
  by (rule class.lattice.intro,
      rule dual_semilattice,
      rule class.semilattice_sup.intro,
      rule dual_order)
    (unfold_locales, auto)

lemma inf_sup_absorb [simp]: "x ⊓ (x ⊔ y) = x"
  by (blast intro: order.antisym inf_le1 inf_greatest sup_ge1)

lemma sup_inf_absorb [simp]: "x ⊔ (x ⊓ y) = x"
  by (blast intro: order.antisym sup_ge1 sup_least inf_le1)

lemmas inf_sup_aci = inf_aci sup_aci

lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2

text ‹Towards distributivity.›

lemma distrib_sup_le: "x ⊔ (y ⊓ z) ≤ (x ⊔ y) ⊓ (x ⊔ z)"
  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)

lemma distrib_inf_le: "(x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)"
  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)

text ‹If you have one of them, you have them all.›

lemma distrib_imp1:
  assumes distrib: "⋀x y z. x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)"
  shows "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
proof-
  have "x ⊔ (y ⊓ z) = (x ⊔ (x ⊓ z)) ⊔ (y ⊓ z)"
    by simp
  also have "… = x ⊔ (z ⊓ (x ⊔ y))"
    by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb)
  also have "… = ((x ⊔ y) ⊓ x) ⊔ ((x ⊔ y) ⊓ z)"
    by (simp add: inf_commute)
  also have "… = (x ⊔ y) ⊓ (x ⊔ z)" by(simp add:distrib)
  finally show ?thesis .
qed

lemma distrib_imp2:
  assumes distrib: "⋀x y z. x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
  shows "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)"
proof-
  have "x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)"
    by simp
  also have "… = x ⊓ (z ⊔ (x ⊓ y))"
    by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb)
  also have "… = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z)"
    by (simp add: sup_commute)
  also have "… = (x ⊓ y) ⊔ (x ⊓ z)" by (simp add:distrib)
  finally show ?thesis .
qed

end


subsubsection ‹Strict order›

context semilattice_inf
begin

lemma less_infI1: "a < x ⟹ a ⊓ b < x"
  by (auto simp add: less_le inf_absorb1 intro: le_infI1)

lemma less_infI2: "b < x ⟹ a ⊓ b < x"
  by (auto simp add: less_le inf_absorb2 intro: le_infI2)

end

context semilattice_sup
begin

lemma less_supI1: "x < a ⟹ x < a ⊔ b"
  using dual_semilattice
  by (rule semilattice_inf.less_infI1)

lemma less_supI2: "x < b ⟹ x < a ⊔ b"
  using dual_semilattice
  by (rule semilattice_inf.less_infI2)

end


subsection ‹Distributive lattices›

class distrib_lattice = lattice +
  assumes sup_inf_distrib1: "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"

context distrib_lattice
begin

lemma sup_inf_distrib2: "(y ⊓ z) ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)"
  by (simp add: sup_commute sup_inf_distrib1)

lemma inf_sup_distrib1: "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)"
  by (rule distrib_imp2 [OF sup_inf_distrib1])

lemma inf_sup_distrib2: "(y ⊔ z) ⊓ x = (y ⊓ x) ⊔ (z ⊓ x)"
  by (simp add: inf_commute inf_sup_distrib1)

lemma dual_distrib_lattice: "class.distrib_lattice sup (≥) (>) inf"
  by (rule class.distrib_lattice.intro, rule dual_lattice)
    (unfold_locales, fact inf_sup_distrib1)

lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2

lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2

lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2

end


subsection ‹Bounded lattices›

class bounded_semilattice_inf_top = semilattice_inf + order_top
begin

sublocale inf_top: semilattice_neutr inf top
  + inf_top: semilattice_neutr_order inf top less_eq less
proof
  show "x ⊓ ⊤ = x" for x
    by (rule inf_absorb1) simp
qed

lemma inf_top_left: "⊤ ⊓ x = x"
  by (fact inf_top.left_neutral)

lemma inf_top_right: "x ⊓ ⊤ = x"
  by (fact inf_top.right_neutral)

lemma inf_eq_top_iff: "x ⊓ y = ⊤ ⟷ x = ⊤ ∧ y = ⊤"
  by (fact inf_top.eq_neutr_iff)

lemma top_eq_inf_iff: "⊤ = x ⊓ y ⟷ x = ⊤ ∧ y = ⊤"
  by (fact inf_top.neutr_eq_iff)

end

class bounded_semilattice_sup_bot = semilattice_sup + order_bot
begin

sublocale sup_bot: semilattice_neutr sup bot
  + sup_bot: semilattice_neutr_order sup bot greater_eq greater
proof
  show "x ⊔ ⊥ = x" for x
    by (rule sup_absorb1) simp
qed

lemma sup_bot_left: "⊥ ⊔ x = x"
  by (fact sup_bot.left_neutral)

lemma sup_bot_right: "x ⊔ ⊥ = x"
  by (fact sup_bot.right_neutral)

lemma sup_eq_bot_iff: "x ⊔ y = ⊥ ⟷ x = ⊥ ∧ y = ⊥"
  by (fact sup_bot.eq_neutr_iff)

lemma bot_eq_sup_iff: "⊥ = x ⊔ y ⟷ x = ⊥ ∧ y = ⊥"
  by (fact sup_bot.neutr_eq_iff)

end

class bounded_lattice_bot = lattice + order_bot
begin

subclass bounded_semilattice_sup_bot ..

lemma inf_bot_left [simp]: "⊥ ⊓ x = ⊥"
  by (rule inf_absorb1) simp

lemma inf_bot_right [simp]: "x ⊓ ⊥ = ⊥"
  by (rule inf_absorb2) simp

end

class bounded_lattice_top = lattice + order_top
begin

subclass bounded_semilattice_inf_top ..

lemma sup_top_left [simp]: "⊤ ⊔ x = ⊤"
  by (rule sup_absorb1) simp

lemma sup_top_right [simp]: "x ⊔ ⊤ = ⊤"
  by (rule sup_absorb2) simp

end

class bounded_lattice = lattice + order_bot + order_top
begin

subclass bounded_lattice_bot ..
subclass bounded_lattice_top ..

lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf ⊤ ⊥"
  by unfold_locales (auto simp add: less_le_not_le)

end


subsection ‹‹min/max› as special case of lattice›

context linorder
begin

sublocale min: semilattice_order min less_eq less
  + max: semilattice_order max greater_eq greater
  by standard (auto simp add: min_def max_def)

declare min.absorb1 [simp] min.absorb2 [simp]
  min.absorb3 [simp] min.absorb4 [simp]
  max.absorb1 [simp] max.absorb2 [simp]
  max.absorb3 [simp] max.absorb4 [simp]

lemma min_le_iff_disj: "min x y ≤ z ⟷ x ≤ z ∨ y ≤ z"
  unfolding min_def using linear by (auto intro: order_trans)

lemma le_max_iff_disj: "z ≤ max x y ⟷ z ≤ x ∨ z ≤ y"
  unfolding max_def using linear by (auto intro: order_trans)

lemma min_less_iff_disj: "min x y < z ⟷ x < z ∨ y < z"
  unfolding min_def le_less using less_linear by (auto intro: less_trans)

lemma less_max_iff_disj: "z < max x y ⟷ z < x ∨ z < y"
  unfolding max_def le_less using less_linear by (auto intro: less_trans)

lemma min_less_iff_conj [simp]: "z < min x y ⟷ z < x ∧ z < y"
  unfolding min_def le_less using less_linear by (auto intro: less_trans)

lemma max_less_iff_conj [simp]: "max x y < z ⟷ x < z ∧ y < z"
  unfolding max_def le_less using less_linear by (auto intro: less_trans)

lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)"
  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)"
  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)"
  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)"
  by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)

lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2

lemma split_min [no_atp]: "P (min i j) ⟷ (i ≤ j ⟶ P i) ∧ (¬ i ≤ j ⟶ P j)"
  by (simp add: min_def)

lemma split_max [no_atp]: "P (max i j) ⟷ (i ≤ j ⟶ P j) ∧ (¬ i ≤ j ⟶ P i)"
  by (simp add: max_def)

lemma split_min_lin [no_atp]:
  ‹P (min a b) ⟷ (b = a ⟶ P a) ∧ (a < b ⟶ P a) ∧ (b < a ⟶ P b)›
  by (cases a b rule: linorder_cases) auto

lemma split_max_lin [no_atp]:
  ‹P (max a b) ⟷ (b = a ⟶ P a) ∧ (a < b ⟶ P b) ∧ (b < a ⟶ P a)›
  by (cases a b rule: linorder_cases) auto

end

lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} ⇒ 'a ⇒ 'a)"
  by (auto intro: antisym simp add: min_def fun_eq_iff)

lemma sup_max: "sup = (max :: 'a::{semilattice_sup,linorder} ⇒ 'a ⇒ 'a)"
  by (auto intro: antisym simp add: max_def fun_eq_iff)


subsection ‹Uniqueness of inf and sup›

lemma (in semilattice_inf) inf_unique:
  fixes f  (infixl ‹△› 70)
  assumes le1: "⋀x y. x △ y ≤ x"
    and le2: "⋀x y. x △ y ≤ y"
    and greatest: "⋀x y z. x ≤ y ⟹ x ≤ z ⟹ x ≤ y △ z"
  shows "x ⊓ y = x △ y"
proof (rule order.antisym)
  show "x △ y ≤ x ⊓ y"
    by (rule le_infI) (rule le1, rule le2)
  have leI: "⋀x y z. x ≤ y ⟹ x ≤ z ⟹ x ≤ y △ z"
    by (blast intro: greatest)
  show "x ⊓ y ≤ x △ y"
    by (rule leI) simp_all
qed

lemma (in semilattice_sup) sup_unique:
  fixes f  (infixl ‹∇› 70)
  assumes ge1 [simp]: "⋀x y. x ≤ x ∇ y"
    and ge2: "⋀x y. y ≤ x ∇ y"
    and least: "⋀x y z. y ≤ x ⟹ z ≤ x ⟹ y ∇ z ≤ x"
  shows "x ⊔ y = x ∇ y"
proof (rule order.antisym)
  show "x ⊔ y ≤ x ∇ y"
    by (rule le_supI) (rule ge1, rule ge2)
  have leI: "⋀x y z. x ≤ z ⟹ y ≤ z ⟹ x ∇ y ≤ z"
    by (blast intro: least)
  show "x ∇ y ≤ x ⊔ y"
    by (rule leI) simp_all
qed


subsection ‹Lattice on \<^typ>‹_ ⇒ _››

instantiation "fun" :: (type, semilattice_sup) semilattice_sup
begin

definition "f ⊔ g = (λx. f x ⊔ g x)"

lemma sup_apply [simp, code]: "(f ⊔ g) x = f x ⊔ g x"
  by (simp add: sup_fun_def)

instance
  by standard (simp_all add: le_fun_def)

end

instantiation "fun" :: (type, semilattice_inf) semilattice_inf
begin

definition "f ⊓ g = (λx. f x ⊓ g x)"

lemma inf_apply [simp, code]: "(f ⊓ g) x = f x ⊓ g x"
  by (simp add: inf_fun_def)

instance by standard (simp_all add: le_fun_def)

end

instance "fun" :: (type, lattice) lattice ..

instance "fun" :: (type, distrib_lattice) distrib_lattice
  by standard (rule ext, simp add: sup_inf_distrib1)

instance "fun" :: (type, bounded_lattice) bounded_lattice ..

instantiation "fun" :: (type, uminus) uminus
begin

definition fun_Compl_def: "- A = (λx. - A x)"

lemma uminus_apply [simp, code]: "(- A) x = - (A x)"
  by (simp add: fun_Compl_def)

instance ..

end

instantiation "fun" :: (type, minus) minus
begin

definition fun_diff_def: "A - B = (λx. A x - B x)"

lemma minus_apply [simp, code]: "(A - B) x = A x - B x"
  by (simp add: fun_diff_def)

instance ..

end

end