# 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