|
1440
|
1 |
(* Title: Lattice.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
|
4 |
|
|
|
5 |
Lattices are orders with binary (finitary) infima and suprema.
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
Lattice = Order +
|
|
|
9 |
|
|
|
10 |
axclass
|
|
|
11 |
lattice < order
|
|
|
12 |
ex_inf "ALL x y. EX inf. is_inf x y inf"
|
|
|
13 |
ex_sup "ALL x y. EX sup. is_sup x y sup"
|
|
|
14 |
|
|
|
15 |
consts
|
|
|
16 |
"&&" :: "['a::lattice, 'a] => 'a" (infixl 70)
|
|
|
17 |
"||" :: "['a::lattice, 'a] => 'a" (infixl 65)
|
|
|
18 |
|
|
|
19 |
defs
|
|
|
20 |
inf_def "x && y == @inf. is_inf x y inf"
|
|
|
21 |
sup_def "x || y == @sup. is_sup x y sup"
|
|
|
22 |
|
|
|
23 |
end
|