Theory Lattices

theory Lattices
imports Groups
(*  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 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)

end

text ‹Passive interpretations for boolean operators›

lemma semilattice_neutr_and:
  "semilattice_neutr HOL.conj True"
  by standard auto

lemma semilattice_neutr_or:
  "semilattice_neutr HOL.disj False"
  by standard auto


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)

lemma le_iff_inf: "x ≤ y ⟷ x ⊓ y = x"
  by (auto intro: le_infI1 antisym dest: 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)

lemma mono_inf: "mono f ⟹ f (A ⊓ B) ≤ f A ⊓ f B" for f :: "'a ⇒ 'b::semilattice_inf"
  by (auto simp add: mono_def intro: Lattices.inf_greatest)

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)

lemma le_iff_sup: "x ≤ y ⟷ x ⊔ y = y"
  by (auto intro: le_supI2 antisym dest: 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)

lemma mono_sup: "mono f ⟹ f A ⊔ f B ≤ f (A ⊔ B)" for f :: "'a ⇒ 'b::semilattice_sup"
  by (auto simp add: mono_def intro: Lattices.sup_least)

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 antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
  show "a ⊓ b = b ⊓ a"
    by (rule antisym) (auto simp add: le_inf_iff)
  show "a ⊓ a = a"
    by (rule 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 antisym) auto

lemma inf_absorb2: "y ≤ x ⟹ x ⊓ y = y"
  by (rule 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 antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
  show "a ⊔ b = b ⊔ a"
    by (rule antisym) (auto simp add: le_sup_iff)
  show "a ⊔ a = a"
    by (rule 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 antisym) auto

lemma sup_absorb2: "x ≤ y ⟹ x ⊔ y = y"
  by (rule 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 (op ≥) (op >) 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: antisym inf_le1 inf_greatest sup_ge1)

lemma sup_inf_absorb [simp]: "x ⊔ (x ⊓ y) = x"
  by (blast intro: 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 (op ≥) (op >) 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 and boolean algebras›

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

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

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

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 [simp]: "x ⊔ y = ⊥ ⟷ x = ⊥ ∧ y = ⊥"
  by (simp add: eq_iff)

lemma bot_eq_sup_iff [simp]: "⊥ = x ⊔ y ⟷ x = ⊥ ∧ y = ⊥"
  by (simp add: eq_iff)

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

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 [simp]: "x ⊓ y = ⊤ ⟷ x = ⊤ ∧ y = ⊤"
  by (simp add: eq_iff)

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

class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
  assumes inf_compl_bot: "x ⊓ - x = ⊥"
    and sup_compl_top: "x ⊔ - x = ⊤"
  assumes diff_eq: "x - y = x ⊓ - y"
begin

lemma dual_boolean_algebra:
  "class.boolean_algebra (λx y. x ⊔ - y) uminus sup greater_eq greater inf ⊤ ⊥"
  by (rule class.boolean_algebra.intro,
      rule dual_bounded_lattice,
      rule dual_distrib_lattice)
    (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)

lemma compl_inf_bot [simp]: "- x ⊓ x = ⊥"
  by (simp add: inf_commute inf_compl_bot)

lemma compl_sup_top [simp]: "- x ⊔ x = ⊤"
  by (simp add: sup_commute sup_compl_top)

lemma compl_unique:
  assumes "x ⊓ y = ⊥"
    and "x ⊔ y = ⊤"
  shows "- x = y"
proof -
  have "(x ⊓ - x) ⊔ (- x ⊓ y) = (x ⊓ y) ⊔ (- x ⊓ y)"
    using inf_compl_bot assms(1) by simp
  then have "(- x ⊓ x) ⊔ (- x ⊓ y) = (y ⊓ x) ⊔ (y ⊓ - x)"
    by (simp add: inf_commute)
  then have "- x ⊓ (x ⊔ y) = y ⊓ (x ⊔ - x)"
    by (simp add: inf_sup_distrib1)
  then have "- x ⊓ ⊤ = y ⊓ ⊤"
    using sup_compl_top assms(2) by simp
  then show "- x = y" by simp
qed

lemma double_compl [simp]: "- (- x) = x"
  using compl_inf_bot compl_sup_top by (rule compl_unique)

lemma compl_eq_compl_iff [simp]: "- x = - y ⟷ x = y"
proof
  assume "- x = - y"
  then have "- (- x) = - (- y)" by (rule arg_cong)
  then show "x = y" by simp
next
  assume "x = y"
  then show "- x = - y" by simp
qed

lemma compl_bot_eq [simp]: "- ⊥ = ⊤"
proof -
  from sup_compl_top have "⊥ ⊔ - ⊥ = ⊤" .
  then show ?thesis by simp
qed

lemma compl_top_eq [simp]: "- ⊤ = ⊥"
proof -
  from inf_compl_bot have "⊤ ⊓ - ⊤ = ⊥" .
  then show ?thesis by simp
qed

lemma compl_inf [simp]: "- (x ⊓ y) = - x ⊔ - y"
proof (rule compl_unique)
  have "(x ⊓ y) ⊓ (- x ⊔ - y) = (y ⊓ (x ⊓ - x)) ⊔ (x ⊓ (y ⊓ - y))"
    by (simp only: inf_sup_distrib inf_aci)
  then show "(x ⊓ y) ⊓ (- x ⊔ - y) = ⊥"
    by (simp add: inf_compl_bot)
next
  have "(x ⊓ y) ⊔ (- x ⊔ - y) = (- y ⊔ (x ⊔ - x)) ⊓ (- x ⊔ (y ⊔ - y))"
    by (simp only: sup_inf_distrib sup_aci)
  then show "(x ⊓ y) ⊔ (- x ⊔ - y) = ⊤"
    by (simp add: sup_compl_top)
qed

lemma compl_sup [simp]: "- (x ⊔ y) = - x ⊓ - y"
  using dual_boolean_algebra
  by (rule boolean_algebra.compl_inf)

lemma compl_mono:
  assumes "x ≤ y"
  shows "- y ≤ - x"
proof -
  from assms have "x ⊔ y = y" by (simp only: le_iff_sup)
  then have "- (x ⊔ y) = - y" by simp
  then have "- x ⊓ - y = - y" by simp
  then have "- y ⊓ - x = - y" by (simp only: inf_commute)
  then show ?thesis by (simp only: le_iff_inf)
qed

lemma compl_le_compl_iff [simp]: "- x ≤ - y ⟷ y ≤ x"
  by (auto dest: compl_mono)

lemma compl_le_swap1:
  assumes "y ≤ - x"
  shows "x ≤ -y"
proof -
  from assms have "- (- x) ≤ - y" by (simp only: compl_le_compl_iff)
  then show ?thesis by simp
qed

lemma compl_le_swap2:
  assumes "- y ≤ x"
  shows "- x ≤ y"
proof -
  from assms have "- x ≤ - (- y)" by (simp only: compl_le_compl_iff)
  then show ?thesis by simp
qed

lemma compl_less_compl_iff: "- x < - y ⟷ y < x"  (* TODO: declare [simp] ? *)
  by (auto simp add: less_le)

lemma compl_less_swap1:
  assumes "y < - x"
  shows "x < - y"
proof -
  from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff)
  then show ?thesis by simp
qed

lemma compl_less_swap2:
  assumes "- y < x"
  shows "- x < y"
proof -
  from assms have "- x < - (- y)"
    by (simp only: compl_less_compl_iff)
  then show ?thesis by simp
qed

lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
  by (simp add: inf_sup_aci sup_compl_top)

lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
  by (simp add: inf_sup_aci sup_compl_top)

lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
  by (simp add: inf_sup_aci inf_compl_bot)

lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
  by (simp add: inf_sup_aci inf_compl_bot)

declare inf_compl_bot [simp]
  and sup_compl_top [simp]

lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
  by (simp add: sup_assoc[symmetric])

lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
  using sup_compl_top_left1[of "- x" y] by simp

lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
  by (simp add: inf_assoc[symmetric])

lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
  using inf_compl_bot_left1[of "- x" y] by simp

lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
  by (subst inf_left_commute) simp

end

ML_file "Tools/boolean_algebra_cancel.ML"

simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
  ‹fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv›

simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
  ‹fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv›


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)

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 min_of_mono: "mono f ⟹ min (f m) (f n) = f (min m n)" for f :: "'a ⇒ 'b::linorder"
  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)

lemma max_of_mono: "mono f ⟹ max (f m) (f n) = f (max m n)" for f :: "'a ⇒ 'b::linorder"
  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)

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 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 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 bool}›

instantiation bool :: boolean_algebra
begin

definition bool_Compl_def [simp]: "uminus = Not"

definition bool_diff_def [simp]: "A - B ⟷ A ∧ ¬ B"

definition [simp]: "P ⊓ Q ⟷ P ∧ Q"

definition [simp]: "P ⊔ Q ⟷ P ∨ Q"

instance by standard auto

end

lemma sup_boolI1: "P ⟹ P ⊔ Q"
  by simp

lemma sup_boolI2: "Q ⟹ P ⊔ Q"
  by simp

lemma sup_boolE: "P ⊔ Q ⟹ (P ⟹ R) ⟹ (Q ⟹ R) ⟹ R"
  by auto


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

instance "fun" :: (type, boolean_algebra) boolean_algebra
  by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+


subsection ‹Lattice on unary and binary predicates›

lemma inf1I: "A x ⟹ B x ⟹ (A ⊓ B) x"
  by (simp add: inf_fun_def)

lemma inf2I: "A x y ⟹ B x y ⟹ (A ⊓ B) x y"
  by (simp add: inf_fun_def)

lemma inf1E: "(A ⊓ B) x ⟹ (A x ⟹ B x ⟹ P) ⟹ P"
  by (simp add: inf_fun_def)

lemma inf2E: "(A ⊓ B) x y ⟹ (A x y ⟹ B x y ⟹ P) ⟹ P"
  by (simp add: inf_fun_def)

lemma inf1D1: "(A ⊓ B) x ⟹ A x"
  by (rule inf1E)

lemma inf2D1: "(A ⊓ B) x y ⟹ A x y"
  by (rule inf2E)

lemma inf1D2: "(A ⊓ B) x ⟹ B x"
  by (rule inf1E)

lemma inf2D2: "(A ⊓ B) x y ⟹ B x y"
  by (rule inf2E)

lemma sup1I1: "A x ⟹ (A ⊔ B) x"
  by (simp add: sup_fun_def)

lemma sup2I1: "A x y ⟹ (A ⊔ B) x y"
  by (simp add: sup_fun_def)

lemma sup1I2: "B x ⟹ (A ⊔ B) x"
  by (simp add: sup_fun_def)

lemma sup2I2: "B x y ⟹ (A ⊔ B) x y"
  by (simp add: sup_fun_def)

lemma sup1E: "(A ⊔ B) x ⟹ (A x ⟹ P) ⟹ (B x ⟹ P) ⟹ P"
  by (simp add: sup_fun_def) iprover

lemma sup2E: "(A ⊔ B) x y ⟹ (A x y ⟹ P) ⟹ (B x y ⟹ P) ⟹ P"
  by (simp add: sup_fun_def) iprover

text ‹ ┉ Classical introduction rule: no commitment to ‹A› vs ‹B›.›

lemma sup1CI: "(¬ B x ⟹ A x) ⟹ (A ⊔ B) x"
  by (auto simp add: sup_fun_def)

lemma sup2CI: "(¬ B x y ⟹ A x y) ⟹ (A ⊔ B) x y"
  by (auto simp add: sup_fun_def)

end