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"

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

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"

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
next
show "a ❙≤ a" for a
next
fix a b
assume "a ❙≤ b" "b ❙≤ a"
then have "a = a ❙* b" "a ❙* b = b"
then show "a = b" by simp
next
fix a b c
assume "a ❙≤ b" "b ❙≤ c"
then have "a = a ❙* b" "b = b ❙* c"
then have "a = a ❙* (b ❙* c)"
by simp
then have "a = (a ❙* b) ❙* c"
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"

lemma cobounded2 [simp]: "a ❙* b ❙≤ b"

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)"
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"

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)

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)"
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)"
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)"

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)"

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 = ⊥"

lemma bot_eq_sup_iff [simp]: "⊥ = x ⊔ y ⟷ x = ⊥ ∧ y = ⊥"

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 = ⊤"

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 = ⊥"

lemma compl_sup_top [simp]: "- x ⊔ x = ⊤"

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)"
then have "- x ⊓ (x ⊔ y) = y ⊓ (x ⊔ - x)"
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) = ⊥"
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) = ⊤"
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] ? *)

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"

lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"

lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"

lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"

declare inf_compl_bot [simp]
and sup_compl_top [simp]

lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"

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"

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)"

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

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"

instance

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"

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)"

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"

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"

lemma inf2I: "A x y ⟹ B x y ⟹ (A ⊓ B) x y"

lemma inf1E: "(A ⊓ B) x ⟹ (A x ⟹ B x ⟹ P) ⟹ P"

lemma inf2E: "(A ⊓ B) x y ⟹ (A x y ⟹ B x y ⟹ P) ⟹ P"

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"

lemma sup2I1: "A x y ⟹ (A ⊔ B) x y"

lemma sup1I2: "B x ⟹ (A ⊔ B) x"

lemma sup2I2: "B x y ⟹ (A ⊔ B) x y"

lemma sup1E: "(A ⊔ B) x ⟹ (A x ⟹ P) ⟹ (B x ⟹ P) ⟹ P"

lemma sup2E: "(A ⊔ B) x y ⟹ (A x y ⟹ P) ⟹ (B x y ⟹ P) ⟹ P"