Theory Lattice

(*File: Lattice.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory Lattice imports Main begin

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

typedecl L (*The lattice*)

  bottom :: L and
  LEQ :: "L  L  bool" and
  LUB :: "L  L  L"
  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›