| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/SIFPL/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 845 B |
|
Quelle Lattice.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(*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
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01