A key part of mathematics is proofs, on this site I would like to include proofs in a consistant way across all the topics, I am therefore using a program called Isabelle which is a proof assistant. More about this program on this page.
This is taken from Isabelle code (from this site) but I have not put the complete code here, just an outline.
In mathematics, a join-semilattice (or upper semilattice) is a partially ordered set that has a join (a least upper bound) for any nonempty finite subset. Dually, a meet-semilattice (or lower semilattice) is a partially ordered set which has a meet (or greatest lower bound) for any nonempty finite subset. Every join-semilattice is a meet-semilattice in the inverse order and vice versa.
Semilattices can also be defined algebraically: join and meet are associative, commutative, idempotent binary operations, and any such operation induces a partial order (and the respective inverse order) such that the result of the operation for any two elements is the least upper bound (or greatest lower bound) of the elements with respect to this partial order.
A lattice is a partially ordered set that is both a meet- and join-semilattice with respect to the same partial order. Algebraically, a lattice is a set with two associative, commutative idempotent binary operations linked by corresponding absorption laws.
Abstract Semilattice
A lattice has both a join and a meet operation but a semilattice has only one of these operatiors.
Join and meet are associative, commutative, idempotent binary operations.
Idempotent means:
From which we can derive:
- a /\ (a /\ b) = a /\ b
- a \/ (a \/ b) = a \/ b
There is also a right-hand version of these.
Absorptive means:
- a \/ (a /\ b) = a /\ (a \/ b) = a
This is represented in Isabelle code (from this site) by starting with an abelian group, which gives associative and commutitive binary operation (as discussed on this page) and adds the idempotent axiom like this:
So the 'f' can represent either '/\' or '\/' depending on wheter it is an infimum (meet) or supremum (join) semilattice.
A lattice is then built from one of each. |
locale semilattice = abel_semigroup +
assumes idem [simp]: "f a a = a"
begin
lemma left_idem [simp]: "f a (f a b) = f a b"
by (simp add: assoc [symmetric])
lemma right_idem [simp]: "f (f a b) b = f a b"
by (simp add: assoc)
end |
Idempotent semigroup
class ab_semigroup_idem_mult = ab_semigroup_mult +
assumes mult_idem: "x * x = x" |
Semilattice
class inf =
fixes inf :: "'a => 'a => 'a" (infixl "\" 70)
class sup =
fixes sup :: "'a => 'a => 'a" (infixl "\" 65)
subsection {* Concrete lattices *}
notation
less_eq (infix "\" 50) and
less (infix "\" 50)
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 |
Lattice
class lattice = semilattice_inf + semilattice_sup |
Dual lattice
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 |
Introduction and Elimination Rules
infimum also known as meet (a /\ b) or greatest lower bound.
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 (rule 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 [simp]:
"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])
lemma inf_mono: "a \ c ==> b \ d ==> a \ b \ c \ d"
by (fast intro: inf_greatest le_infI1 le_infI2)
lemma mono_inf:
fixes f :: "'a => 'b::semilattice_inf"
shows "mono f ==> f (A \ B) \ f A \ f B"
by (auto simp add: mono_def intro: Lattices.inf_greatest)
end |
supremum also known as the join (a \/ b) or least upper bound.
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 (rule 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 [simp]:
"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])
lemma sup_mono: "a \ c ==> b \ d ==> a \ b \ c \ d"
by (fast intro: sup_least le_supI1 le_supI2)
lemma mono_sup:
fixes f :: "'a => 'b::semilattice_sup"
shows "mono f ==> f A \ f B \ f (A \ B)"
by (auto simp add: mono_def intro: Lattices.sup_least)
end |
Equational laws
subsubsection {* Equational laws *}
sublocale semilattice_inf < inf!: semilattice inf
proof
fix a b c
show "(a \ b) \ c = a \ (b \ c)"
by (rule antisym) (auto intro: le_infI1 le_infI2)
show "a \ b = b \ a"
by (rule antisym) auto
show "a \ a = a"
by (rule antisym) auto
qed
context semilattice_inf
begin
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
sublocale semilattice_sup < sup!: semilattice sup
proof
fix a b c
show "(a \ b) \ c = a \ (b \ c)"
by (rule antisym) (auto intro: le_supI1 le_supI2)
show "a \ b = b \ a"
by (rule antisym) auto
show "a \ a = a"
by (rule antisym) auto
qed
context semilattice_sup
begin
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 D: "!!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: D 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:D)
finally show ?thesis .
qed
lemma distrib_imp2:
assumes D: "!!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: D 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:D)
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_lattice_bot = lattice + bot
begin
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 [simp]:
"⊥ \ x = x"
by (rule sup_absorb2) simp
lemma sup_bot_right [simp]:
"x \ ⊥ = x"
by (rule sup_absorb1) simp
lemma sup_eq_bot_iff [simp]:
"x \ y = ⊥ <-> x = ⊥ ∧ y = ⊥"
by (simp add: eq_iff)
end
class bounded_lattice_top = lattice + top
begin
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 [simp]:
"\ \ x = x"
by (rule inf_absorb2) simp
lemma inf_top_right [simp]:
"x \ \ = x"
by (rule inf_absorb1) simp
lemma inf_eq_top_iff [simp]:
"x \ y = \ <-> x = \ ∧ y = \"
by (simp add: eq_iff)
end
class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
begin
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:
"x \ y ==> - y \ - x"
proof -
assume "x \ y"
then 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 "- y \ |