(*File: Lattice.thy*) (*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*) theory Lattice imports Main begin section‹Lattices›
text‹In preparation of the encoding of the type system of Hunt and
, we define some abstract type of lattices, together with the
$\bot$, $\sqsubseteq$ and $\sqcup$, and some obvious
.›
typedecl L (*The lattice*)
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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
