IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

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 $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

$IsJoinSemilattice (L, r) \equiv$ $r \subseteq L \times L \land IsPartOrder (L, r) \land (\forall x \in L . \forall y \in L . 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

$IsMeetSemilattice (L, r) \equiv$ $r \subseteq L \times L \land IsPartOrder (L, r) \land (\forall x \in L . \forall y \in L . 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 is a lattice on L \equiv IsJoinSemilattice (L, r) \land IsMeetSemilattice (L, r)$

Join is a binary operation whose value on a pair $⟨ x, y ⟩$ is defined as the supremum of the set ${x, y}$ .

definition

$Join (L, r) \equiv {⟨ p, Supremum (r, {fst (p), snd (p)}) ⟩ . p \in L \times L}$

Meet is a binary operation whose value on a pair $⟨ x, y ⟩$ is defined as the infimum of the set ${x, y}$ .

definition

$Meet (L, r) \equiv {⟨ p, Infimum (r, {fst (p), snd (p)}) ⟩ . p \in L \times L}$

Linear order is a lattice.

lemma lin_is_latt:

assumes $r \subseteq L \times 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

with assms have

IsMeetSemilattice (L, r)

unfolding IsLinOrder_def, IsMeetSemilattice_def using inf_sup_two_el(1)

moreover

from assms,

IsPartOrder (L, r)

have

IsJoinSemilattice (L, r)

unfolding IsLinOrder_def, IsJoinSemilattice_def using inf_sup_two_el(3)

ultimately show

t h e s i s

unfolding IsAlattice_def

qed

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

lemma join_is_binop:

assumes $IsJoinSemilattice (L, r)$

shows

Join (L, r) : L \times L \to L

proof

from assms have

\forall p \in L \times L . Supremum (r, {fst (p), snd (p)}) \in L

unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space

then show

t h e s i s

unfolding Join_def using ZF_fun_from_total

qed

The value of $Join (L, r)$ on a pair $⟨ x, y ⟩$ is the supremum of the set ${x, y}$ , hence its is greater or equal than both.

lemma join_val:

assumes $IsJoinSemilattice (L, r)$ , $x \in L$ , $y \in L$

defines $j \equiv Join (L, r) ⟨ x, y ⟩$

shows

j \in L

j = Supremum (r, {x, y})

⟨ x, j ⟩ \in r

⟨ y, j ⟩ \in r

proof

from assms(1) have

Join (L, r) : L \times L \to L

using join_is_binop

with assms(2,3,4) show

j = Supremum (r, {x, y})

unfolding Join_def using ZF_fun_from_tot_val

from assms(2,3,4),

Join (L, r) : L \times L \to L

show

j \in L

using apply_funtype

from assms(1,2,3) have

r \subseteq L \times L

antisym (r)

HasAminimum (r, ⋂ z \in {x, y} . r {z})

unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def

with

j = Supremum (r, {x, y})

show

⟨ x, j ⟩ \in r

and

⟨ y, j ⟩ \in r

using sup_in_space(2)

qed

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

lemma meet_is_binop:

assumes $IsMeetSemilattice (L, r)$

shows

Meet (L, r) : L \times L \to L

proof

from assms have

\forall p \in L \times L . Infimum (r, {fst (p), snd (p)}) \in L

unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space

then show

t h e s i s

unfolding Meet_def using ZF_fun_from_total

qed

The value of $Meet (L, r)$ on a pair $⟨ x, y ⟩$ is the infimum of the set ${x, y}$ , hence is less or equal than both.

lemma meet_val:

assumes $IsMeetSemilattice (L, r)$ , $x \in L$ , $y \in L$

defines $m \equiv Meet (L, r) ⟨ x, y ⟩$

shows

m \in L

m = Infimum (r, {x, y})

⟨ m, x ⟩ \in r

⟨ m, y ⟩ \in r

proof

from assms(1) have

Meet (L, r) : L \times L \to L

using meet_is_binop

with assms(2,3,4) show

m = Infimum (r, {x, y})

unfolding Meet_def using ZF_fun_from_tot_val

from assms(2,3,4),

Meet (L, r) : L \times L \to L

show

m \in L

using apply_funtype

from assms(1,2,3) have

r \subseteq L \times L

antisym (r)

HasAmaximum (r, ⋂ z \in {x, y} . r^{- 1} {z})

unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def

with

m = Infimum (r, {x, y})

show

⟨ m, x ⟩ \in r

and

⟨ m, y ⟩ \in r

using inf_in_space(2)

qed

In a (nonempty) meet semi-lattice the relation down-directs the set.

lemma meet_down_directs:

assumes $IsMeetSemilattice (L, r)$ , $L \neq 0$

shows

r down-directs L

proof

{

fix

x

y

assume

x \in L

y \in L

let

m = Meet (L, r) ⟨ x, y ⟩

from assms(1),

x \in L

y \in L

have

m \in L

⟨ m, x ⟩ \in r

⟨ m, y ⟩ \in r

using meet_val

}

hence

\forall x \in L . \forall y \in L . \exists m \in L . ⟨ m, x ⟩ \in r \land ⟨ m, y ⟩ \in r

with assms(2) show

t h e s i s

unfolding DownDirects_def

qed

In a (nonempty) join semi-lattice the relation up-directs the set.

lemma join_up_directs:

assumes $IsJoinSemilattice (L, r)$ , $L \neq 0$

shows

r up-directs L

proof

{

fix

x

y

assume

x \in L

y \in L

let

m = Join (L, r) ⟨ x, y ⟩

from assms(1),

x \in L

y \in L

have

m \in L

⟨ x, m ⟩ \in r

⟨ y, m ⟩ \in r

using join_val

}

hence

\forall x \in L . \forall y \in L . \exists m \in L . ⟨ x, m ⟩ \in r \land ⟨ y, m ⟩ \in r

with assms(2) show

t h e s i s

unfolding UpDirects_def

qed

The next locale defines a a notation for join-semilattice. We will use the $⊔$ symbol rather than more common $\lor$ to avoid confusion with logical "or".

locale join_semilatt

assumes joinLatt: $IsJoinSemilattice (L, r)$

defines $x ⊔ y \equiv Join (L, r) ⟨ x, y ⟩$

defines $sup A \equiv 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 ⊔ y \in L

and

x ⊔ y = sup {x, y}

proof

from joinLatt, assms have

Join (L, r) ⟨ x, y ⟩ \in L

using join_is_binop, apply_funtype

thus

x ⊔ y \in L

from joinLatt, assms have

Join (L, r) ⟨ x, y ⟩ = Supremum (r, {x, y})

using join_val(2)

thus

x ⊔ y = 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 ⊔ (y ⊔ z) = x ⊔ y ⊔ z

proof

from joinLatt, assms(2,3) have

x ⊔ (y ⊔ z) = x ⊔ (sup {y, z})

using join_val(2)

also

from assms, joinLatt have

. . . = sup {sup {x}, sup {y, z}}

unfolding IsJoinSemilattice_def, IsPartOrder_def using join_props, sup_inf_singl(2)

also

have

. . . = sup {x, y, z}

proof

let

T = {{x}, {y, z}}

from joinLatt have

r \subseteq L \times L

antisym (r)

trans (r)

unfolding IsJoinSemilattice_def, IsPartOrder_def

moreover

from joinLatt, assms have

\forall T \in T . HasAsupremum (r, T)

unfolding IsJoinSemilattice_def, IsPartOrder_def using sup_inf_singl(1)

moreover

from joinLatt, assms have

HasAsupremum (r, {Supremum (r, T) . T \in T})

unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space(1), sup_inf_singl(2)

ultimately have

Supremum (r, {Supremum (r, T) . T \in T}) = Supremum (r, ⋃ T)

by (rule sup_sup )

moreover

have

{Supremum (r, T) . T \in T} = {sup {x}, sup {y, z}}

and

⋃ T = {x, y, z}

ultimately show

(sup {sup {x}, sup {y, z}}) = sup {x, y, z}

qed

also

have

. . . = sup {sup {x, y}, sup {z}}

proof

let

T = {{x, y}, {z}}

from joinLatt have

r \subseteq L \times L

antisym (r)

trans (r)

unfolding IsJoinSemilattice_def, IsPartOrder_def

moreover

from joinLatt, assms have

\forall T \in T . HasAsupremum (r, T)

unfolding IsJoinSemilattice_def, IsPartOrder_def using sup_inf_singl(1)

moreover

from joinLatt, assms have

HasAsupremum (r, {Supremum (r, T) . T \in T})

unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space(1), sup_inf_singl(2)

ultimately have

Supremum (r, {Supremum (r, T) . T \in T}) = Supremum (r, ⋃ T)

by (rule sup_sup )

moreover

have

{Supremum (r, T) . T \in T} = {sup {x, y}, sup {z}}

and

⋃ T = {x, y, z}

ultimately show

(sup {x, y, z}) = sup {sup {x, y}, sup {z}}

qed

also

from assms, joinLatt have

. . . = sup {sup {x, y}, z}

unfolding IsJoinSemilattice_def, IsPartOrder_def using join_props, sup_inf_singl(2)

also

from assms, joinLatt have

. . . = (sup {x, y}) ⊔ z

unfolding IsJoinSemilattice_def, IsPartOrder_def using join_props

also

from joinLatt, assms(1,2) have

. . . = x ⊔ y ⊔ z

using join_val(2)

finally show

x ⊔ (y ⊔ z) = x ⊔ y ⊔ z

qed

Join is idempotent.

lemma (in join_semilatt) join_idempotent:

assumes $x \in L$

shows

x ⊔ x = x

using joinLatt, assms, join_val(2), 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 $⊓$ symbol to denote join, giving it ab bit higher precedence.

locale meet_semilatt

assumes meetLatt: $IsMeetSemilattice (L, r)$

defines $x ⊓ y \equiv Meet (L, r) ⟨ x, y ⟩$

defines $inf A \equiv 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 ⊓ y \in L

and

x ⊓ y = inf {x, y}

proof

from meetLatt, assms have

Meet (L, r) ⟨ x, y ⟩ \in L

using meet_is_binop, apply_funtype

thus

x ⊓ y \in L

from meetLatt, assms have

Meet (L, r) ⟨ x, y ⟩ = Infimum (r, {x, y})

using meet_val(2)

thus

x ⊓ y = 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 ⊓ (y ⊓ z) = x ⊓ y ⊓ z

proof

from meetLatt, assms(2,3) have

x ⊓ (y ⊓ z) = x ⊓ (inf {y, z})

using meet_val

also

from assms, meetLatt have

. . . = inf {inf {x}, inf {y, z}}

unfolding IsMeetSemilattice_def, IsPartOrder_def using meet_props, sup_inf_singl(4)

also

have

. . . = inf {x, y, z}

proof

let

T = {{x}, {y, z}}

from meetLatt have

r \subseteq L \times L

antisym (r)

trans (r)

unfolding IsMeetSemilattice_def, IsPartOrder_def

moreover

from meetLatt, assms have

\forall T \in T . HasAnInfimum (r, T)

unfolding IsMeetSemilattice_def, IsPartOrder_def using sup_inf_singl(3)

moreover

from meetLatt, assms have

HasAnInfimum (r, {Infimum (r, T) . T \in T})

unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space(1), sup_inf_singl(4)

ultimately have

Infimum (r, {Infimum (r, T) . T \in T}) = Infimum (r, ⋃ T)

by (rule inf_inf )

moreover

have

{Infimum (r, T) . T \in T} = {inf {x}, inf {y, z}}

and

⋃ T = {x, y, z}

ultimately show

(inf {inf {x}, inf {y, z}}) = inf {x, y, z}

qed

also

have

. . . = inf {inf {x, y}, inf {z}}

proof

let

T = {{x, y}, {z}}

from meetLatt have

r \subseteq L \times L

antisym (r)

trans (r)

unfolding IsMeetSemilattice_def, IsPartOrder_def

moreover

from meetLatt, assms have

\forall T \in T . HasAnInfimum (r, T)

unfolding IsMeetSemilattice_def, IsPartOrder_def using sup_inf_singl(3)

moreover

from meetLatt, assms have

HasAnInfimum (r, {Infimum (r, T) . T \in T})

unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space(1), sup_inf_singl(4)

ultimately have

Infimum (r, {Infimum (r, T) . T \in T}) = Infimum (r, ⋃ T)

by (rule inf_inf )

moreover

have

{Infimum (r, T) . T \in T} = {inf {x, y}, inf {z}}

and

⋃ T = {x, y, z}

ultimately show

(inf {x, y, z}) = inf {inf {x, y}, inf {z}}

qed

also

from assms, meetLatt have

. . . = inf {inf {x, y}, z}

unfolding IsMeetSemilattice_def, IsPartOrder_def using meet_props, sup_inf_singl(4)

also

from assms, meetLatt have

. . . = (inf {x, y}) ⊓ z

unfolding IsMeetSemilattice_def, IsPartOrder_def using meet_props

also

from meetLatt, assms(1,2) have

. . . = x ⊓ y ⊓ z

using meet_val

finally show

x ⊓ (y ⊓ z) = x ⊓ y ⊓ z

qed

Meet is idempotent.

lemma (in meet_semilatt) meet_idempotent:

assumes $x \in L$

shows

x ⊓ x = x

using meetLatt, assms, meet_val, IsMeetSemilattice_def, IsPartOrder_def, sup_inf_singl(4)

end

lemma Order_ZF_1_L2:

assumes $IsLinOrder (X, r)$

shows

IsPartOrder (X, r)

Definition of IsLinOrder:

IsLinOrder (X, r) \equiv antisym (r) \land trans (r) \land (r is total on X)

Definition of IsMeetSemilattice:

IsMeetSemilattice (L, r) \equiv

r \subseteq L \times L \land IsPartOrder (L, r) \land (\forall x \in L . \forall y \in L . HasAnInfimum (r, {x, y}))

lemma inf_sup_two_el:

assumes $antisym (r)$ , $r is total on X$ , $x \in X$ , $y \in X$

shows

HasAnInfimum (r, {x, y})

Minimum (r, {x, y}) = Infimum (r, {x, y})

HasAsupremum (r, {x, y})

Maximum (r, {x, y}) = Supremum (r, {x, y})

Definition of IsJoinSemilattice:

IsJoinSemilattice (L, r) \equiv

r \subseteq L \times L \land IsPartOrder (L, r) \land (\forall x \in L . \forall y \in L . HasAsupremum (r, {x, y}))

lemma inf_sup_two_el:

assumes $antisym (r)$ , $r is total on X$ , $x \in X$ , $y \in X$

shows

HasAnInfimum (r, {x, y})

Minimum (r, {x, y}) = Infimum (r, {x, y})

HasAsupremum (r, {x, y})

Maximum (r, {x, y}) = Supremum (r, {x, y})

Definition of IsAlattice:

r is a lattice on L \equiv IsJoinSemilattice (L, r) \land IsMeetSemilattice (L, r)

Definition of IsPartOrder:

IsPartOrder (X, r) \equiv refl (X, r) \land antisym (r) \land trans (r)

Definition of HasAsupremum:

HasAsupremum (r, A) \equiv HasAminimum (r, ⋂ a \in A . r {a})

lemma sup_in_space:

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

shows

Supremum (r, A) \in X

and

\forall x \in A . ⟨ x, Supremum (r, A) ⟩ \in r

Definition of Join:

Join (L, r) \equiv {⟨ p, Supremum (r, {fst (p), snd (p)}) ⟩ . p \in L \times L}

lemma ZF_fun_from_total:

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

shows

{⟨ x, b (x) ⟩ . x \in X} : X \to Y

lemma join_is_binop:

assumes $IsJoinSemilattice (L, r)$

shows

Join (L, r) : L \times L \to L

lemma ZF_fun_from_tot_val:

assumes $f : X \to Y$ , $x \in X$ and $f = {⟨ x, b (x) ⟩ . x \in X}$

shows

f (x) = b (x)

and

b (x) \in Y

lemma sup_in_space:

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

shows

Supremum (r, A) \in X

and

\forall x \in A . ⟨ x, Supremum (r, A) ⟩ \in r

Definition of HasAnInfimum:

HasAnInfimum (r, A) \equiv HasAmaximum (r, ⋂ a \in A . r^{- 1} {a})

lemma inf_in_space:

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

shows

Infimum (r, A) \in X

and

\forall x \in A . ⟨ Infimum (r, A), x ⟩ \in r

Definition of Meet:

Meet (L, r) \equiv {⟨ p, Infimum (r, {fst (p), snd (p)}) ⟩ . p \in L \times L}

lemma meet_is_binop:

assumes $IsMeetSemilattice (L, r)$

shows

Meet (L, r) : L \times L \to L

lemma inf_in_space:

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

shows

Infimum (r, A) \in X

and

\forall x \in A . ⟨ Infimum (r, A), x ⟩ \in r

lemma meet_val:

assumes $IsMeetSemilattice (L, r)$ , $x \in L$ , $y \in L$

defines $m \equiv Meet (L, r) ⟨ x, y ⟩$

shows

m \in L

m = Infimum (r, {x, y})

⟨ m, x ⟩ \in r

⟨ m, y ⟩ \in r

Definition of DownDirects:

r down-directs X \equiv X \neq 0 \land (\forall x \in X . \forall y \in X . \exists z \in X . ⟨ z, x ⟩ \in r \land ⟨ z, y ⟩ \in r)

lemma join_val:

assumes $IsJoinSemilattice (L, r)$ , $x \in L$ , $y \in L$

defines $j \equiv Join (L, r) ⟨ x, y ⟩$

shows

j \in L

j = Supremum (r, {x, y})

⟨ x, j ⟩ \in r

⟨ y, j ⟩ \in r

Definition of UpDirects:

r up-directs X \equiv X \neq 0 \land (\forall x \in X . \forall y \in X . \exists z \in X . ⟨ x, z ⟩ \in r \land ⟨ y, z ⟩ \in r)

lemma join_val:

assumes $IsJoinSemilattice (L, r)$ , $x \in L$ , $y \in L$

defines $j \equiv Join (L, r) ⟨ x, y ⟩$

shows

j \in L

j = Supremum (r, {x, y})

⟨ x, j ⟩ \in r

⟨ y, j ⟩ \in r

lemma (in join_semilatt) join_props:

assumes $x \in L$ , $y \in L$

shows

x ⊔ y \in L

and

x ⊔ y = sup {x, y}

lemma sup_inf_singl:

assumes $antisym (r)$ , $refl (X, r)$ , $z \in X$

shows

HasAsupremum (r, {z})

Supremum (r, {z}) = z

and

HasAnInfimum (r, {z})

Infimum (r, {z}) = z

lemma sup_inf_singl:

assumes $antisym (r)$ , $refl (X, r)$ , $z \in X$

shows

HasAsupremum (r, {z})

Supremum (r, {z}) = z

and

HasAnInfimum (r, {z})

Infimum (r, {z}) = z

lemma sup_in_space:

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

shows

Supremum (r, A) \in X

and

\forall x \in A . ⟨ x, Supremum (r, A) ⟩ \in r

lemma sup_sup:

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

shows

HasAsupremum (r, ⋃ T)

and

Supremum (r, {Supremum (r, T) . T \in T}) = Supremum (r, ⋃ T)

lemma meet_val:

assumes $IsMeetSemilattice (L, r)$ , $x \in L$ , $y \in L$

defines $m \equiv Meet (L, r) ⟨ x, y ⟩$

shows

m \in L

m = Infimum (r, {x, y})

⟨ m, x ⟩ \in r

⟨ m, y ⟩ \in r

lemma (in meet_semilatt) meet_props:

assumes $x \in L$ , $y \in L$

shows

x ⊓ y \in L

and

x ⊓ y = inf {x, y}

lemma sup_inf_singl:

assumes $antisym (r)$ , $refl (X, r)$ , $z \in X$

shows

HasAsupremum (r, {z})

Supremum (r, {z}) = z

and

HasAnInfimum (r, {z})

Infimum (r, {z}) = z

lemma sup_inf_singl:

assumes $antisym (r)$ , $refl (X, r)$ , $z \in X$

shows

HasAsupremum (r, {z})

Supremum (r, {z}) = z

and

HasAnInfimum (r, {z})

Infimum (r, {z}) = z

lemma inf_in_space:

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

shows

Infimum (r, A) \in X

and

\forall x \in A . ⟨ Infimum (r, A), x ⟩ \in r

lemma inf_inf:

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