IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory Lattice_ZF imports Order_ZF_1a func1
begin

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.

Semilattices

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 \( \text{IsPartOrder}(L,r) \).

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

\( \text{IsJoinSemilattice}(L,r) \equiv \) \( r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAsupremum}(r,\{x,y\})) \)

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

\( \text{IsMeetSemilattice}(L,r) \equiv \) \( r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAnInfimum}(r,\{x,y\})) \)

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

\( r \text{ is a lattice on } L \equiv \text{IsJoinSemilattice}(L,r) \wedge \text{IsMeetSemilattice}(L,r) \)

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

\( \text{Join}(L,r) \equiv \{\langle p, \text{Supremum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\} \)

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

\( \text{Meet}(L,r) \equiv \{\langle p, \text{Infimum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\} \)

In a join-semilattice join is indeed a binary operation.

lemma join_is_binop:

assumes \( \text{IsJoinSemilattice}(L,r) \)

shows \( \text{Join}(L,r) : L\times L \rightarrow L \)proof
from assms have \( \forall p \in L\times L.\ \text{Supremum}(r,\{\text{fst}(p),\text{snd}(p)\}) \in L \) unfolding IsJoinSemilattice_def , IsPartOrder_def , HasAsupremum_def using sup_in_space
then show \( thesis \) unfolding Join_def using ZF_fun_from_total
qed

The value of \( \text{Join}(L,r) \) on a pair \(\langle x,y\rangle\) is the supremum of the set \(\{ x,y\}\).

lemma join_val:

assumes \( \text{IsJoinSemilattice}(L,r) \), \( x\in L \), \( y\in L \)

shows \( \text{Join}(L,r)\langle x,y\rangle = \text{Supremum}(r,\{x,y\}) \)proof
from assms(1) have \( \text{Join}(L,r) : L\times L \rightarrow L \) using join_is_binop
with assms(2,3) show \( thesis \) unfolding Join_def using ZF_fun_from_tot_val
qed

In a meet-semilattice meet is indeed a binary operation.

lemma meet_is_binop:

assumes \( \text{IsMeetSemilattice}(L,r) \)

shows \( \text{Meet}(L,r) : L\times L \rightarrow L \)proof
from assms have \( \forall p \in L\times L.\ \text{Infimum}(r,\{\text{fst}(p),\text{snd}(p)\}) \in L \) unfolding IsMeetSemilattice_def , IsPartOrder_def , HasAnInfimum_def using inf_in_space
then show \( thesis \) unfolding Meet_def using ZF_fun_from_total
qed

The value of \( \text{Meet}(L,r) \) on a pair \(\langle x,y\rangle\) is the infimum of the set \(\{ x,y\}\).

lemma meet_val:

assumes \( \text{IsMeetSemilattice}(L,r) \), \( x\in L \), \( y\in L \)

shows \( \text{Meet}(L,r)\langle x,y\rangle = \text{Infimum}(r,\{x,y\}) \)proof
from assms(1) have \( \text{Meet}(L,r) : L\times L \rightarrow L \) using meet_is_binop
with assms(2,3) show \( thesis \) unfolding Meet_def using ZF_fun_from_tot_val
qed

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

assumes joinLatt: \( \text{IsJoinSemilattice}(L,r) \)

defines \( x \sqcup y \equiv \text{Join}(L,r)\langle x,y\rangle \)

defines \( \text{sup}A \equiv \text{Supremum}(r,A) \)

Join of the elements of the lattice is in the lattice.

lemma (in join_semilatt) join_props:

assumes \( x\in L \), \( y\in L \)

shows \( x\sqcup y \in L \) and \( x\sqcup y = \text{sup}\{x,y\} \)proof
from joinLatt, assms have \( \text{Join}(L,r)\langle x,y\rangle \in L \) using join_is_binop , apply_funtype
thus \( x\sqcup y \in L \)
from joinLatt, assms have \( \text{Join}(L,r)\langle x,y\rangle = \text{Supremum}(r,\{x,y\}) \) using join_val
thus \( x\sqcup y = \text{sup}\{x,y\} \)
qed

Join is associative.

lemma (in join_semilatt) join_assoc:

assumes \( x\in L \), \( y\in L \), \( z\in L \)

shows \( x\sqcup (y\sqcup z) = x\sqcup y\sqcup z \)proof
from joinLatt, assms(2,3) have \( x\sqcup (y\sqcup z) = x\sqcup (\text{sup}\{y,z\}) \) using join_val
also
from assms, joinLatt have \( .\ .\ .\ = \text{sup}\{\text{sup}\{x\}, \text{sup}\{y,z\}\} \) unfolding IsJoinSemilattice_def , IsPartOrder_def using join_props , sup_inf_singl(2)
also
have \( .\ .\ .\ = \text{sup}\{x,y,z\} \)proof
let \( \mathcal{T} = \{\{x\},\{y,z\}\} \)
from joinLatt have \( r \subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \) unfolding IsJoinSemilattice_def , IsPartOrder_def
moreover
from joinLatt, assms have \( \forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T) \) unfolding IsJoinSemilattice_def , IsPartOrder_def using sup_inf_singl(1)
moreover
from joinLatt, assms have \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \) unfolding IsJoinSemilattice_def , IsPartOrder_def , HasAsupremum_def using sup_in_space(1) , sup_inf_singl(2)
ultimately have \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} ) \) by (rule sup_sup )
moreover
have \( \{ \text{Supremum}(r,T).\ T\in \mathcal{T} \} = \{\text{sup}\{x\}, \text{sup}\{y,z\}\} \) and \( \bigcup \mathcal{T} = \{x,y,z\} \)
ultimately show \( (\text{sup}\{\text{sup}\{x\}, \text{sup}\{y,z\}\}) = \text{sup}\{x,y,z\} \)
qed
also
have \( .\ .\ .\ = \text{sup}\{\text{sup}\{x,y\}, \text{sup}\{z\}\} \)proof
let \( \mathcal{T} = \{\{x,y\},\{z\}\} \)
from joinLatt have \( r \subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \) unfolding IsJoinSemilattice_def , IsPartOrder_def
moreover
from joinLatt, assms have \( \forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T) \) unfolding IsJoinSemilattice_def , IsPartOrder_def using sup_inf_singl(1)
moreover
from joinLatt, assms have \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \) unfolding IsJoinSemilattice_def , IsPartOrder_def , HasAsupremum_def using sup_in_space(1) , sup_inf_singl(2)
ultimately have \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} ) \) by (rule sup_sup )
moreover
have \( \{ \text{Supremum}(r,T).\ T\in \mathcal{T} \} = \{\text{sup}\{x,y\}, \text{sup}\{z\}\} \) and \( \bigcup \mathcal{T} = \{x,y,z\} \)
ultimately show \( (\text{sup}\{x,y,z\}) = \text{sup}\{\text{sup}\{x,y\}, \text{sup}\{z\}\} \)
qed
also
from assms, joinLatt have \( .\ .\ .\ = \text{sup}\{\text{sup}\{x,y\}, z\} \) unfolding IsJoinSemilattice_def , IsPartOrder_def using join_props , sup_inf_singl(2)
also
from assms, joinLatt have \( .\ .\ .\ = (\text{sup}\{x,y\}) \sqcup z \) unfolding IsJoinSemilattice_def , IsPartOrder_def using join_props
also
from joinLatt, assms(1,2) have \( .\ .\ .\ = x\sqcup y\sqcup z \) using join_val
finally show \( x\sqcup (y\sqcup z) = x\sqcup y\sqcup z \)
qed

Join is idempotent.

lemma (in join_semilatt) join_idempotent:

assumes \( x\in L \)

shows \( x\sqcup x = x \) using joinLatt , assms , join_val , IsJoinSemilattice_def , IsPartOrder_def , sup_inf_singl(2)

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

assumes meetLatt: \( \text{IsMeetSemilattice}(L,r) \)

defines \( x \sqcap y \equiv \text{Meet}(L,r)\langle x,y\rangle \)

defines \( \text{inf}A \equiv \text{Infimum}(r,A) \)

Meet of the elements of the lattice is in the lattice.

lemma (in meet_semilatt) meet_props:

assumes \( x\in L \), \( y\in L \)

shows \( x\sqcap y \in L \) and \( x\sqcap y = \text{inf}\{x,y\} \)proof
from meetLatt, assms have \( \text{Meet}(L,r)\langle x,y\rangle \in L \) using meet_is_binop , apply_funtype
thus \( x\sqcap y \in L \)
from meetLatt, assms have \( \text{Meet}(L,r)\langle x,y\rangle = \text{Infimum}(r,\{x,y\}) \) using meet_val
thus \( x\sqcap y = \text{inf}\{x,y\} \)
qed

Meet is associative.

lemma (in meet_semilatt) meet_assoc:

assumes \( x\in L \), \( y\in L \), \( z\in L \)

shows \( x\sqcap (y\sqcap z) = x\sqcap y\sqcap z \)proof
from meetLatt, assms(2,3) have \( x\sqcap (y\sqcap z) = x\sqcap (\text{inf}\{y,z\}) \) using meet_val
also
from assms, meetLatt have \( .\ .\ .\ = \text{inf}\{\text{inf}\{x\}, \text{inf}\{y,z\}\} \) unfolding IsMeetSemilattice_def , IsPartOrder_def using meet_props , sup_inf_singl(4)
also
have \( .\ .\ .\ = \text{inf}\{x,y,z\} \)proof
let \( \mathcal{T} = \{\{x\},\{y,z\}\} \)
from meetLatt have \( r \subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \) unfolding IsMeetSemilattice_def , IsPartOrder_def
moreover
from meetLatt, assms have \( \forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T) \) unfolding IsMeetSemilattice_def , IsPartOrder_def using sup_inf_singl(3)
moreover
from meetLatt, assms have \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \) unfolding IsMeetSemilattice_def , IsPartOrder_def , HasAnInfimum_def using inf_in_space(1) , sup_inf_singl(4)
ultimately have \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} ) \) by (rule inf_inf )
moreover
have \( \{ \text{Infimum}(r,T).\ T\in \mathcal{T} \} = \{\text{inf}\{x\}, \text{inf}\{y,z\}\} \) and \( \bigcup \mathcal{T} = \{x,y,z\} \)
ultimately show \( (\text{inf}\{\text{inf}\{x\}, \text{inf}\{y,z\}\}) = \text{inf}\{x,y,z\} \)
qed
also
have \( .\ .\ .\ = \text{inf}\{\text{inf}\{x,y\}, \text{inf}\{z\}\} \)proof
let \( \mathcal{T} = \{\{x,y\},\{z\}\} \)
from meetLatt have \( r \subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \) unfolding IsMeetSemilattice_def , IsPartOrder_def
moreover
from meetLatt, assms have \( \forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T) \) unfolding IsMeetSemilattice_def , IsPartOrder_def using sup_inf_singl(3)
moreover
from meetLatt, assms have \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \) unfolding IsMeetSemilattice_def , IsPartOrder_def , HasAnInfimum_def using inf_in_space(1) , sup_inf_singl(4)
ultimately have \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} ) \) by (rule inf_inf )
moreover
have \( \{ \text{Infimum}(r,T).\ T\in \mathcal{T} \} = \{\text{inf}\{x,y\}, \text{inf}\{z\}\} \) and \( \bigcup \mathcal{T} = \{x,y,z\} \)
ultimately show \( (\text{inf}\{x,y,z\}) = \text{inf}\{\text{inf}\{x,y\}, \text{inf}\{z\}\} \)
qed
also
from assms, meetLatt have \( .\ .\ .\ = \text{inf}\{\text{inf}\{x,y\}, z\} \) unfolding IsMeetSemilattice_def , IsPartOrder_def using meet_props , sup_inf_singl(4)
also
from assms, meetLatt have \( .\ .\ .\ = (\text{inf}\{x,y\}) \sqcap z \) unfolding IsMeetSemilattice_def , IsPartOrder_def using meet_props
also
from meetLatt, assms(1,2) have \( .\ .\ .\ = x\sqcap y\sqcap z \) using meet_val
finally show \( x\sqcap (y\sqcap z) = x\sqcap y\sqcap z \)
qed

Meet is idempotent.

lemma (in meet_semilatt) meet_idempotent:

assumes \( x\in L \)

shows \( x\sqcap x = x \) using meetLatt , assms , meet_val , IsMeetSemilattice_def , IsPartOrder_def , sup_inf_singl(4)
end
Definition of IsJoinSemilattice: \( \text{IsJoinSemilattice}(L,r) \equiv \) \( r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAsupremum}(r,\{x,y\})) \)
Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv (\text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r)) \)
Definition of HasAsupremum: \( \text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
lemma sup_in_space:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)

shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)
Definition of Join: \( \text{Join}(L,r) \equiv \{\langle p, \text{Supremum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\} \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
lemma join_is_binop:

assumes \( \text{IsJoinSemilattice}(L,r) \)

shows \( \text{Join}(L,r) : L\times L \rightarrow L \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \)
Definition of IsMeetSemilattice: \( \text{IsMeetSemilattice}(L,r) \equiv \) \( r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAnInfimum}(r,\{x,y\})) \)
Definition of HasAnInfimum: \( \text{HasAnInfimum}(r,A) \equiv \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
lemma inf_in_space:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)

shows \( \text{Infimum}(r,A) \in X \) and \( \forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r \)
Definition of Meet: \( \text{Meet}(L,r) \equiv \{\langle p, \text{Infimum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\} \)
lemma meet_is_binop:

assumes \( \text{IsMeetSemilattice}(L,r) \)

shows \( \text{Meet}(L,r) : L\times L \rightarrow L \)
lemma join_val:

assumes \( \text{IsJoinSemilattice}(L,r) \), \( x\in L \), \( y\in L \)

shows \( \text{Join}(L,r)\langle x,y\rangle = \text{Supremum}(r,\{x,y\}) \)
lemma (in join_semilatt) join_props:

assumes \( x\in L \), \( y\in L \)

shows \( x\sqcup y \in L \) and \( x\sqcup y = \text{sup}\{x,y\} \)
lemma sup_inf_singl:

assumes \( \text{antisym}(r) \), \( \text{refl}(X,r) \), \( z\in X \)

shows \( \text{HasAsupremum}(r,\{z\}) \), \( \text{Supremum}(r,\{z\}) = z \) and \( \text{HasAnInfimum}(r,\{z\}) \), \( \text{Infimum}(r,\{z\}) = z \)
lemma sup_inf_singl:

assumes \( \text{antisym}(r) \), \( \text{refl}(X,r) \), \( z\in X \)

shows \( \text{HasAsupremum}(r,\{z\}) \), \( \text{Supremum}(r,\{z\}) = z \) and \( \text{HasAnInfimum}(r,\{z\}) \), \( \text{Infimum}(r,\{z\}) = z \)
lemma sup_in_space:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)

shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)
lemma sup_sup:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T) \), \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \)

shows \( \text{HasAsupremum}(r,\bigcup \mathcal{T} ) \) and \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} ) \)
lemma meet_val:

assumes \( \text{IsMeetSemilattice}(L,r) \), \( x\in L \), \( y\in L \)

shows \( \text{Meet}(L,r)\langle x,y\rangle = \text{Infimum}(r,\{x,y\}) \)
lemma (in meet_semilatt) meet_props:

assumes \( x\in L \), \( y\in L \)

shows \( x\sqcap y \in L \) and \( x\sqcap y = \text{inf}\{x,y\} \)
lemma sup_inf_singl:

assumes \( \text{antisym}(r) \), \( \text{refl}(X,r) \), \( z\in X \)

shows \( \text{HasAsupremum}(r,\{z\}) \), \( \text{Supremum}(r,\{z\}) = z \) and \( \text{HasAnInfimum}(r,\{z\}) \), \( \text{Infimum}(r,\{z\}) = z \)
lemma sup_inf_singl:

assumes \( \text{antisym}(r) \), \( \text{refl}(X,r) \), \( z\in X \)

shows \( \text{HasAsupremum}(r,\{z\}) \), \( \text{Supremum}(r,\{z\}) = z \) and \( \text{HasAnInfimum}(r,\{z\}) \), \( \text{Infimum}(r,\{z\}) = z \)
lemma inf_in_space:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)

shows \( \text{Infimum}(r,A) \in X \) and \( \forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r \)
lemma inf_inf:

assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T) \), \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \)

shows \( \text{HasAnInfimum}(r,\bigcup \mathcal{T} ) \) and \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} ) \)
60
100
12
12