(* 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 \<^bold>* a = a"
begin
lemma left_idem [simp]:
"a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
by (simp add: assoc [symmetric])
lemma right_idem [simp]:
"(a \<^bold>* b) \<^bold>* b = a \<^bold>* 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 \<^bold>\ b \ a = a \<^bold>* b"
and strict_order_iff:
"a \<^bold>< b \ a = a \<^bold>* b \ a \ b"
begin
lemma orderI:
"a = a \<^bold>* b \ a \<^bold>\ b"
by (simp add: order_iff)
lemma orderE:
assumes "a \<^bold>\ b"
obtains "a = a \<^bold>* b"
using assms
by (unfold order_iff)
sublocale ordering less_eq less
proof
show "a \<^bold>< b \ a \<^bold>\ b \ a \ b" for a b
by (simp add: order_iff strict_order_iff)
next
show "a \<^bold>\ a" for a
by (simp add: order_iff)
next
fix a b
assume "a \<^bold>\ b" "b \<^bold>\ a"
then have "a = a \<^bold>* b" "a \<^bold>* b = b"
by (simp_all add: order_iff commute)
then show "a = b" by simp
next
fix a b c
assume "a \<^bold>\ b" "b \<^bold>\ c"
then have "a = a \<^bold>* b" "b = b \<^bold>* c"
by (simp_all add: order_iff commute)
then have "a = a \<^bold>* (b \<^bold>* c)"
by simp
then have "a = (a \<^bold>* b) \<^bold>* c"
by (simp add: assoc)
with ‹a = a
🚫* b
› [symmetric]
have "a = a \<^bold>* c" by simp
then show "a \<^bold>\ c" by (rule orderI)
qed
lemma cobounded1 [simp]:
"a \<^bold>* b \<^bold>\ a"
by (simp add: order_iff commute)
lemma cobounded2 [simp]:
"a \<^bold>* b \<^bold>\ b"
by (simp add: order_iff)
lemma boundedI:
assumes "a \<^bold>\ b" and "a \<^bold>\ c"
shows "a \<^bold>\ b \<^bold>* c"
proof (rule orderI)
from assms
obtain "a \<^bold>* b = a" and "a \<^bold>* c = a"
by (auto elim!: orderE)
then show "a = a \<^bold>* (b \<^bold>* c)"
by (simp add: assoc [symmetric])
qed
lemma boundedE:
assumes "a \<^bold>\ b \<^bold>* c"
obtains "a \<^bold>\ b" and "a \<^bold>\ c"
using assms
by (blast intro: trans cobounded1 cobounded2)
lemma bounded_iff [simp]:
"a \<^bold>\ b \<^bold>* c \ a \<^bold>\ b \ a \<^bold>\ c"
by (blast intro: boundedI elim: boundedE)
lemma strict_boundedE:
assumes "a \<^bold>< b \<^bold>* c"
obtains "a \<^bold>< b" and "a \<^bold>< c"
using assms
by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
lemma coboundedI1:
"a \<^bold>\ c \ a \<^bold>* b \<^bold>\ c"
by (rule trans) auto
lemma coboundedI2:
"b \<^bold>\ c \ a \<^bold>* b \<^bold>\ c"
by (rule trans) auto
lemma strict_coboundedI1:
"a \<^bold>< c \ a \<^bold>* b \<^bold>< c"
using irrefl
by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order
elim: strict_boundedE)
lemma strict_coboundedI2:
"b \<^bold>< c \ a \<^bold>* b \<^bold>< c"
using strict_coboundedI1 [of b c a]
by (simp add: commute)
lemma mono:
"a \<^bold>\ c \ b \<^bold>\ d \ a \<^bold>* b \<^bold>\ c \<^bold>* d"
by (blast intro: boundedI coboundedI1 coboundedI2)
lemma absorb1:
"a \<^bold>\ b \ a \<^bold>* b = a"
by (rule antisym) (auto simp: refl)
lemma absorb2:
"b \<^bold>\ a \ a \<^bold>* b = b"
by (rule antisym) (auto simp: refl)
lemma absorb3:
"a \<^bold>< b \ a \<^bold>* b = a"
by (rule absorb1) (rule strict_implies_order)
lemma absorb4:
"b \<^bold>< a \ a \<^bold>* b = b"
by (rule absorb2) (rule strict_implies_order)
lemma absorb_iff1:
"a \<^bold>\ b \ a \<^bold>* b = a"
using order_iff
by auto
lemma absorb_iff2:
"b \<^bold>\ a \ a \<^bold>* 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
"\<^bold>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 🍋‹_ ==> _››
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
