(*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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet am 2026-06-10)
¤
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.
