Theory Lattice_ZF
section ‹Semilattices and Lattices›
theory Lattice_ZF imports Order_ZF_1a func1 Finite_ZF
begin
text‹ Lattices can be introduced in algebraic way as commutative idempotent ($x\cdot x =x$)
semigroups or as partial orders with some additional properties. These two approaches are
equivalent. In this theory we will use the order-theoretic approach. ›
subsection‹Semilattices›
text‹ We start with a relation $r$ which is a partial order on a set $L$. Such situation is defined
in ‹Order_ZF› as the predicate ‹IsPartOrder(L,r)›. ›
text‹ A partially ordered $(L,r)$ set is a join-semilattice if each two-element subset of $L$
has a supremum (i.e. the least upper bound). ›
definition
"IsJoinSemilattice(L,r) ≡
r⊆L×L ∧ IsPartOrder(L,r) ∧ (∀x∈L. ∀y∈L. HasAsupremum(r,{x,y}))"
text‹ A partially ordered $(L,r)$ set is a meet-semilattice if each two-element subset of $L$
has an infimum (i.e. the greatest lower bound). ›
definition
"IsMeetSemilattice(L,r) ≡
r⊆L×L ∧ IsPartOrder(L,r) ∧ (∀x∈L. ∀y∈L. HasAnInfimum(r,{x,y}))"
text‹ Join is a binary operation whose value on a pair $\langle x,y\rangle$
is defined as the supremum of the set $\{ x,y\}$. ›
definition
"Join(L,r) ≡ {⟨p,Supremum(r,{fst(p),snd(p)})⟩ . p ∈ L×L}"
text‹ Meet is a binary operation whose value on a pair $\langle x,y\rangle$
is defined as the infimum of the set $\{ x,y\}$.›
definition
"Meet(L,r) ≡ {⟨p,Infimum(r,{fst(p),snd(p)})⟩ . p ∈ L×L}"
text‹ In a join-semilattice join is indeed a binary operation. ›
lemma join_is_binop: assumes "IsJoinSemilattice(L,r)"
shows "Join(L,r) : L×L → L"
proof -
from assms have "∀p ∈ L×L. Supremum(r,{fst(p),snd(p)}) ∈ L"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def using sup_in_space
by auto
then show ?thesis unfolding Join_def using ZF_fun_from_total by simp
qed
text‹The value of ‹Join(L,r)› on a pair $\langle x,y\rangle$ is the supremum
of the set $\{ x,y\}$, hence its is greater or equal than both.›
lemma join_val:
assumes "IsJoinSemilattice(L,r)" "x∈L" "y∈L"
defines "j ≡ Join(L,r)`⟨x,y⟩"
shows "j∈L" "j = Supremum(r,{x,y})" "⟨x,j⟩ ∈ r" "⟨y,j⟩ ∈ r"
proof -
from assms(1) have "Join(L,r) : L×L → L" using join_is_binop by simp
with assms(2,3,4) show "j = Supremum(r,{x,y})" unfolding Join_def using ZF_fun_from_tot_val
by auto
from assms(2,3,4) ‹Join(L,r) : L×L → L› show "j∈L" using apply_funtype by simp
from assms(1,2,3) have "r ⊆ L×L" "antisym(r)" "HasAminimum(r,⋂z∈{x,y}. r``{z})"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def by auto
with ‹j = Supremum(r,{x,y})› show "⟨x,j⟩ ∈ r" and "⟨y,j⟩ ∈ r"
using sup_in_space(2) by auto
qed
text‹Join of $x,y$ is less or equal than any upper bound for $\{ x,y\}$. ›
lemma join_least_upbound:
assumes "IsJoinSemilattice(L,r)" "⟨x,z⟩ ∈ r" "⟨y,z⟩ ∈ r"
shows "⟨Join(L,r)`⟨x,y⟩,z⟩ ∈ r"
proof -
from assms have "x∈L" "y∈L"
unfolding IsJoinSemilattice_def by auto
with assms show ?thesis using join_val sup_leq_up_bnd
unfolding IsJoinSemilattice_def IsPartOrder_def by simp
qed
text‹ In a meet-semilattice meet is indeed a binary operation. ›
lemma meet_is_binop: assumes "IsMeetSemilattice(L,r)"
shows "Meet(L,r) : L×L → L"
proof -
from assms have "∀p ∈ L×L. Infimum(r,{fst(p),snd(p)}) ∈ L"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def using inf_in_space
by auto
then show ?thesis unfolding Meet_def using ZF_fun_from_total by simp
qed
text‹ The value of ‹Meet(L,r)› on a pair $\langle x,y\rangle$ is the infimum
of the set $\{ x,y\}$, hence is less or equal than both. ›
lemma meet_val:
assumes "IsMeetSemilattice(L,r)" "x∈L" "y∈L"
defines "m ≡ Meet(L,r)`⟨x,y⟩"
shows "m∈L" "m = Infimum(r,{x,y})" "⟨m,x⟩ ∈ r" "⟨m,y⟩ ∈ r"
proof -
from assms(1) have "Meet(L,r) : L×L → L" using meet_is_binop by simp
with assms(2,3,4) show "m = Infimum(r,{x,y})" unfolding Meet_def using ZF_fun_from_tot_val
by auto
from assms(2,3,4) ‹Meet(L,r) : L×L → L› show "m∈L" using apply_funtype by simp
from assms(1,2,3) have "r ⊆ L×L" "antisym(r)" "HasAmaximum(r,⋂z∈{x,y}. r-``{z})"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def by auto
with ‹m = Infimum(r,{x,y})› show "⟨m,x⟩ ∈ r" and "⟨m,y⟩ ∈ r"
using inf_in_space(2) by auto
qed
text‹In a join semilattice a union of two sets that have suprema has a supremum.›
lemma join_semilat_sup_two: assumes "IsJoinSemilattice(L,r)"
"HasAsupremum(r,A)" "HasAsupremum(r,B)"
shows "HasAsupremum(r,A∪B)" and
"Supremum(r,A∪B) = Join(L,r)`⟨Supremum(r,A),Supremum(r,B)⟩"
proof -
let ?S⇩A = "Supremum(r,A)"
let ?S⇩B = "Supremum(r,B)"
from assms have "?S⇩A∈L" "?S⇩B∈L"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def
using sup_in_space by auto
with assms have
I: "Join(L,r)`⟨?S⇩A,?S⇩B⟩ = Supremum(r,{?S⇩A,?S⇩B})" and
II: "r⊆L×L" "antisym(r)" "trans(r)" "∀T∈{A,B}. HasAsupremum(r,T)"
"HasAsupremum(r,{Supremum(r,T). T∈{A,B}})"
using join_val(2) unfolding IsJoinSemilattice_def IsPartOrder_def
by simp_all
from II have "HasAsupremum(r,⋃{A,B})" by (rule sup_sup)
from II have
"Supremum(r,{Supremum(r,T). T∈{A,B}}) = Supremum(r,⋃{A,B})"
by (rule sup_sup)
with ‹HasAsupremum(r,⋃{A,B})› I show
"HasAsupremum(r,A∪B)" and "Supremum(r,A∪B) = Join(L,r)`⟨?S⇩A,?S⇩B⟩"
by simp_all
qed
text‹In a meet semilattice a union of two sets that have infima has an infimum.›
lemma meet_semilat_inf_two: assumes "IsMeetSemilattice(L,r)"
"HasAnInfimum(r,A)" "HasAnInfimum(r,B)"
shows "HasAnInfimum(r,A∪B)" and
"Infimum(r,A∪B) = Meet(L,r)`⟨Infimum(r,A),Infimum(r,B)⟩"
proof -
let ?I⇩A = "Infimum(r,A)"
let ?I⇩B = "Infimum(r,B)"
from assms have "?I⇩A∈L" "?I⇩B∈L"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def
using inf_in_space by auto
with assms have
I: "Meet(L,r)`⟨?I⇩A,?I⇩B⟩ = Infimum(r,{?I⇩A,?I⇩B})" and
II: "r⊆L×L" "antisym(r)" "trans(r)" "∀T∈{A,B}. HasAnInfimum(r,T)"
"HasAnInfimum(r,{Infimum(r,T). T∈{A,B}})"
using meet_val(2) unfolding IsMeetSemilattice_def IsPartOrder_def
by simp_all
from II have "HasAnInfimum(r,⋃{A,B})" by (rule inf_inf)
from II have
"Infimum(r,{Infimum(r,T). T∈{A,B}}) = Infimum(r,⋃{A,B})"
by (rule inf_inf)
with ‹HasAnInfimum(r,⋃{A,B})› I show
"HasAnInfimum(r,A∪B)" and "Infimum(r,A∪B) = Meet(L,r)`⟨?I⇩A,?I⇩B⟩"
by simp_all
qed
text‹In a join semilattice every nonempty finite set has a supremum.›
lemma join_semilat_fin_sup:
assumes "IsJoinSemilattice(L,r)" "N∈FinPow(L)" "N≠∅"
shows "HasAsupremum(r,N)"
proof -
let ?C = "{B∈Pow(L). HasAsupremum(r,B)}"
from assms(1,2) have "∀x∈N. {x}∈?C"
unfolding IsJoinSemilattice_def IsPartOrder_def FinPow_def
using sup_inf_singl(1) by auto
from assms(1) have "∀A∈?C. ∀B∈?C. A∪B ∈ ?C"
using join_semilat_sup_two by auto
with assms(2,3) ‹∀x∈N. {x}∈?C› have "N∈?C"
by (rule union_two_union_fin_nempty)
thus "HasAsupremum(r,N)" by simp
qed
text‹In a meet semilattice every nonempty finite set has a infimum.›
lemma meet_semilat_fin_inf:
assumes "IsMeetSemilattice(L,r)" "N∈FinPow(L)" "N≠∅"
shows "HasAnInfimum(r,N)"
proof -
let ?C = "{B∈Pow(L). HasAnInfimum(r,B)}"
from assms(1,2) have "∀x∈N. {x}∈?C"
unfolding IsMeetSemilattice_def IsPartOrder_def FinPow_def
using sup_inf_singl(3) by auto
from assms(1) have "∀A∈?C. ∀B∈?C. A∪B ∈ ?C"
using meet_semilat_inf_two by auto
with assms(2,3) ‹∀x∈N. {x}∈?C› have "N∈?C"
by (rule union_two_union_fin_nempty)
thus "HasAnInfimum(r,N)" by simp
qed
text‹In a (nonempty) meet semi-lattice the relation down-directs the set. ›
lemma meet_down_directs: assumes "IsMeetSemilattice(L,r)" "L≠0"
shows "r {down-directs} L"
proof -
{ fix x y assume "x∈L" "y∈L"
let ?m = "Meet(L,r)`⟨x,y⟩"
from assms(1) ‹x∈L› ‹y∈L› have "?m∈L" "⟨?m,x⟩ ∈ r" "⟨?m,y⟩ ∈ r"
using meet_val by auto
} hence "∀x∈L. ∀y∈L. ∃m∈L. ⟨m,x⟩ ∈ r ∧⟨m,y⟩ ∈ r"
by blast
with assms(2) show ?thesis unfolding DownDirects_def by simp
qed
text‹In a (nonempty) join semi-lattice the relation up-directs the set. ›
lemma join_up_directs: assumes "IsJoinSemilattice(L,r)" "L≠0"
shows "r {up-directs} L"
proof -
{ fix x y assume "x∈L" "y∈L"
let ?m = "Join(L,r)`⟨x,y⟩"
from assms(1) ‹x∈L› ‹y∈L› have "?m∈L" "⟨x,?m⟩ ∈ r" "⟨y,?m⟩ ∈ r"
using join_val by auto
} hence "∀x∈L. ∀y∈L. ∃m∈L. ⟨x,m⟩ ∈ r ∧⟨y,m⟩ ∈ r"
by blast
with assms(2) show ?thesis unfolding UpDirects_def by simp
qed
text‹ The next locale defines a a notation for join-semilattice. We will use the $\sqcup$ symbol
rather than more common $\vee$ to avoid confusion with logical "or". ›
locale join_semilatt =
fixes L
fixes r
assumes joinLatt: "IsJoinSemilattice(L,r)"
fixes join (infixl "⊔" 71)
defines join_def [simp]: "x ⊔ y ≡ Join(L,r)`⟨x,y⟩"
fixes sup ("sup _" )
defines sup_def [simp]: "sup A ≡ Supremum(r,A)"
text‹ Join of the elements of the lattice is in the lattice. ›
lemma (in join_semilatt) join_props: assumes "x∈L" "y∈L"
shows "x⊔y ∈ L" and "x⊔y = sup {x,y}"
proof -
from joinLatt assms have "Join(L,r)`⟨x,y⟩ ∈ L" using join_is_binop apply_funtype
by blast
thus "x⊔y ∈ L" by simp
from joinLatt assms have "Join(L,r)`⟨x,y⟩ = Supremum(r,{x,y})" using join_val(2)
by simp
thus "x⊔y = sup {x,y}" by simp
qed
text‹Join is associative.›
lemma (in join_semilatt) join_assoc: assumes "x∈L" "y∈L" "z∈L"
shows "x⊔(y⊔z) = x⊔y⊔z"
proof -
from joinLatt assms(2,3) have "x⊔(y⊔z) = x⊔(sup {y,z})" using join_val(2) by simp
also from assms joinLatt have "... = sup {sup {x}, sup {y,z}}"
unfolding IsJoinSemilattice_def IsPartOrder_def using join_props sup_inf_singl(2)
by auto
also have "... = sup {x,y,z}"
proof -
let ?𝒯 = "{{x},{y,z}}"
from joinLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsJoinSemilattice_def IsPartOrder_def by auto
moreover from joinLatt assms have "∀T∈?𝒯. HasAsupremum(r,T)"
unfolding IsJoinSemilattice_def IsPartOrder_def using sup_inf_singl(1) by blast
moreover from joinLatt assms have "HasAsupremum(r,{Supremum(r,T).T∈?𝒯})"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def
using sup_in_space(1) sup_inf_singl(2) by auto
ultimately have "Supremum(r,{Supremum(r,T).T∈?𝒯}) = Supremum(r,⋃?𝒯)" by (rule sup_sup)
moreover have "{Supremum(r,T).T∈?𝒯} = {sup {x}, sup {y,z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(sup {sup {x}, sup {y,z}}) = sup {x,y,z}" by simp
qed
also have "... = sup {sup {x,y}, sup {z}}"
proof -
let ?𝒯 = "{{x,y},{z}}"
from joinLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsJoinSemilattice_def IsPartOrder_def by auto
moreover from joinLatt assms have "∀T∈?𝒯. HasAsupremum(r,T)"
unfolding IsJoinSemilattice_def IsPartOrder_def using sup_inf_singl(1) by blast
moreover from joinLatt assms have "HasAsupremum(r,{Supremum(r,T).T∈?𝒯})"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def
using sup_in_space(1) sup_inf_singl(2) by auto
ultimately have "Supremum(r,{Supremum(r,T).T∈?𝒯}) = Supremum(r,⋃?𝒯)" by (rule sup_sup)
moreover have "{Supremum(r,T).T∈?𝒯} = {sup {x,y}, sup {z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(sup {x,y,z}) = sup {sup {x,y}, sup {z}}" by auto
qed
also from assms joinLatt have "... = sup {sup {x,y}, z}"
unfolding IsJoinSemilattice_def IsPartOrder_def using join_props sup_inf_singl(2)
by auto
also from assms joinLatt have "... = (sup {x,y}) ⊔ z "
unfolding IsJoinSemilattice_def IsPartOrder_def using join_props by auto
also from joinLatt assms(1,2) have "... = x⊔y⊔z" using join_val(2) by simp
finally show "x⊔(y⊔z) = x⊔y⊔z" by simp
qed
text‹ Join is idempotent. ›
lemma (in join_semilatt) join_idempotent: assumes "x∈L" shows "x⊔x = x"
using joinLatt assms join_val(2) IsJoinSemilattice_def IsPartOrder_def sup_inf_singl(2)
by auto
text‹ The ‹meet_semilatt› locale is the dual of the join-semilattice locale defined above.
We will use the $\sqcap$ symbol to denote join, giving it ab bit higher precedence.›
locale meet_semilatt =
fixes L
fixes r
assumes meetLatt: "IsMeetSemilattice(L,r)"
fixes join (infixl "⊓" 72)
defines join_def [simp]: "x ⊓ y ≡ Meet(L,r)`⟨x,y⟩"
fixes sup ("inf _" )
defines sup_def [simp]: "inf A ≡ Infimum(r,A)"
text‹ Meet of the elements of the lattice is in the lattice. ›
lemma (in meet_semilatt) meet_props: assumes "x∈L" "y∈L"
shows "x⊓y ∈ L" and "x⊓y = inf {x,y}"
proof -
from meetLatt assms have "Meet(L,r)`⟨x,y⟩ ∈ L" using meet_is_binop apply_funtype
by blast
thus "x⊓y ∈ L" by simp
from meetLatt assms have "Meet(L,r)`⟨x,y⟩ = Infimum(r,{x,y})" using meet_val(2) by blast
thus "x⊓y = inf {x,y}" by simp
qed
text‹ Meet is associative. ›
lemma (in meet_semilatt) meet_assoc: assumes "x∈L" "y∈L" "z∈L"
shows "x⊓(y⊓z) = x⊓y⊓z"
proof -
from meetLatt assms(2,3) have "x⊓(y⊓z) = x⊓(inf {y,z})" using meet_val by simp
also from assms meetLatt have "... = inf {inf {x}, inf {y,z}}"
unfolding IsMeetSemilattice_def IsPartOrder_def using meet_props sup_inf_singl(4)
by auto
also have "... = inf {x,y,z}"
proof -
let ?𝒯 = "{{x},{y,z}}"
from meetLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsMeetSemilattice_def IsPartOrder_def by auto
moreover from meetLatt assms have "∀T∈?𝒯. HasAnInfimum(r,T)"
unfolding IsMeetSemilattice_def IsPartOrder_def using sup_inf_singl(3) by blast
moreover from meetLatt assms have "HasAnInfimum(r,{Infimum(r,T).T∈?𝒯})"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def
using inf_in_space(1) sup_inf_singl(4) by auto
ultimately have "Infimum(r,{Infimum(r,T).T∈?𝒯}) = Infimum(r,⋃?𝒯)" by (rule inf_inf)
moreover have "{Infimum(r,T).T∈?𝒯} = {inf {x}, inf {y,z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(inf {inf {x}, inf {y,z}}) = inf {x,y,z}" by simp
qed
also have "... = inf {inf {x,y}, inf {z}}"
proof -
let ?𝒯 = "{{x,y},{z}}"
from meetLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsMeetSemilattice_def IsPartOrder_def by auto
moreover from meetLatt assms have "∀T∈?𝒯. HasAnInfimum(r,T)"
unfolding IsMeetSemilattice_def IsPartOrder_def using sup_inf_singl(3) by blast
moreover from meetLatt assms have "HasAnInfimum(r,{Infimum(r,T).T∈?𝒯})"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def
using inf_in_space(1) sup_inf_singl(4) by auto
ultimately have "Infimum(r,{Infimum(r,T).T∈?𝒯}) = Infimum(r,⋃?𝒯)" by (rule inf_inf)
moreover have "{Infimum(r,T).T∈?𝒯} = {inf {x,y}, inf {z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(inf {x,y,z}) = inf {inf {x,y}, inf {z}}" by auto
qed
also from assms meetLatt have "... = inf {inf {x,y}, z}"
unfolding IsMeetSemilattice_def IsPartOrder_def using meet_props sup_inf_singl(4)
by auto
also from assms meetLatt have "... = (inf {x,y}) ⊓ z "
unfolding IsMeetSemilattice_def IsPartOrder_def using meet_props by auto
also from meetLatt assms(1,2) have "... = x⊓y⊓z" using meet_val by simp
finally show "x⊓(y⊓z) = x⊓y⊓z" by simp
qed
text‹Meet is idempotent.›
lemma (in meet_semilatt) meet_idempotent: assumes "x∈L" shows "x⊓x = x"
using meetLatt assms meet_val IsMeetSemilattice_def IsPartOrder_def sup_inf_singl(4)
by auto
subsection‹Lattices›
text‹Here we study lattices, i.e. structures where both meet and join are defined.›
text‹ A partially ordered $(L,r)$ set is a lattice if it is both join and meet-semilattice, i.e. if
every two element set has a supremum (least upper bound) and infimum (greatest lower bound). ›
definition
IsAlattice (infixl "{is a lattice on}" 90) where
"r {is a lattice on} L ≡ IsJoinSemilattice(L,r) ∧ IsMeetSemilattice(L,r)"
text‹Linear order is a lattice.›
lemma lin_is_latt: assumes "r⊆L×L" and "IsLinOrder(L,r)"
shows "r {is a lattice on} L"
proof -
from assms(2) have "IsPartOrder(L,r)" using Order_ZF_1_L2 by simp
with assms have "IsMeetSemilattice(L,r)" unfolding IsLinOrder_def IsMeetSemilattice_def
using inf_sup_two_el(1) by auto
moreover from assms ‹IsPartOrder(L,r)› have "IsJoinSemilattice(L,r)"
unfolding IsLinOrder_def IsJoinSemilattice_def using inf_sup_two_el(3) by auto
ultimately show ?thesis unfolding IsAlattice_def by simp
qed
subsection‹Complete lattices›
text‹The definition of a lattice requires that every two-element set has a supremum and infimum.
As we show in ‹join_semilat_fin_sup› and ‹meet_semilat_fin_inf› this implies
that every finite subset of the lattice has supremum and infimum.
In this section we study structures in which every nonempty subset (not necessarily finite)
has both supremum and infimum.›
text‹Wikipedia defines a complete lattice as a partially ordered set in which every subset has
both supremum and infimum. The way we define supremum and infimum only nonempty sets can have
infima or suprema so to avoid inconsistency we define a complete lattice as the one in
which all nonempty subsets have both infima and suprema. We also add the assumption that
the carrier is nonempty so that we don't have to repeat that assumption in every proposition
about complete lattices.›
definition
"IsCompleteLattice(r,L) ≡ L≠∅ ∧ r⊆L×L ∧ IsPartOrder(L,r) ∧
(∀A∈Pow(L)∖{∅}. (HasAsupremum(r,A) ∧ HasAnInfimum(r,A)))"
text‹Complete lattices are bounded and have both maximum and minimum.›
lemma compl_lat_bounded: assumes "IsCompleteLattice(r,L)"
shows "HasAmaximum(r,L)" "HasAminimum(r,L)" "IsBounded(L,r)"
proof -
from assms have "Supremum(r,L)∈L" and "Infimum(r,L)∈L"
using sup_in_space(1) inf_in_space(1)
unfolding IsCompleteLattice_def IsPartOrder_def
HasAsupremum_def HasAnInfimum_def by simp_all
with assms show "HasAmaximum(r,L)" "HasAminimum(r,L)" "IsBounded(L,r)"
using sup_is_max(1) inf_is_min(1) Order_ZF_4_L7 Order_ZF_4_L8A
unfolding IsCompleteLattice_def IsPartOrder_def IsBounded_def
by simp_all
qed
end