| changeset 7626 | 5997f35954d7 |
| 7625:94b2a50e69a5 | 7626:5997f35954d7 |
|---|---|
1 (* Title: HOL/BCV/SemiLattice.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1999 TUM |
|
5 |
|
6 Semilattices |
|
7 *) |
|
8 |
|
9 SemiLattice = Plus + |
|
10 |
|
11 constdefs |
|
12 semilat :: "('a::{order,plus} set) => bool" |
|
13 "semilat A == (!x:A. !y:A. x <= x+y) & |
|
14 (!x:A. !y:A. y <= x+y) & |
|
15 (!x:A. !y:A. !z:A. x <= z & y <= z --> x+y <= z) & |
|
16 (!x:A. !y:A. x+y : A)" |
|
17 |
|
18 end |