# Theory Lattice

theory Lattice imports Main begin
section‹Lattices›
text‹In preparation of the encoding of the type system of Hunt and
Sands, we define some abstract type of lattices, together with the
operations $\bot$, $\sqsubseteq$ and $\sqcup$, and some obvious
axioms.›
typedecl L
axiomatization
bottom :: L and
LEQ :: "L ⇒ L ⇒ bool" and
LUB :: "L ⇒ L ⇒ L"
where
LAT1: "LEQ bottom p" and
LAT2: "LEQ p1 p2 ⟹ LEQ p2 p3 ⟹ LEQ p1 p3" and
LAT3: "LEQ p (LUB p q)" and
LAT4: "LUB p q = LUB q p" and
LAT5: "LUB p (LUB q r) = LUB (LUB p q) r" and
LAT6: "LEQ x x" and
LAT7: "p = LUB p p"
text‹End of theory Lattice›
end