src/HOL/AxClasses/Lattice/Lattice.thy
author wenzelm
Tue, 30 May 2000 16:08:38 +0200
changeset 9000 c20d58286a51
parent 2606 27cdd600a3b1
permissions -rw-r--r--
cleaned up;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     1
(*  Title:      Lattice.thy
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     4
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     5
Lattices are orders with binary (finitary) infima and suprema.
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     6
*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     7
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     8
Lattice = Order +
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    10
axclass
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1440
diff changeset
    11
  lattice < partial_order
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    12
  ex_inf       "ALL x y. EX inf. is_inf x y inf"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    13
  ex_sup       "ALL x y. EX sup. is_sup x y sup"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    14
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    15
consts
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    16
  "&&"          :: "['a::lattice, 'a] => 'a"       (infixl 70)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    17
  "||"          :: "['a::lattice, 'a] => 'a"       (infixl 65)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    18
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    19
defs
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    20
  inf_def       "x && y == @inf. is_inf x y inf"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    21
  sup_def       "x || y == @sup. is_sup x y sup"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    22
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    23
end