Lattices

In order to get the definition of a lattice closer to that in the CCL-book, the definitions of reflexivity, transitivity, and antisymmetry were redefined Redefinitions allow for changes in the usage of previously defined constructors. Typical redefinitions cover:

• changes to the signature of a constructor, for example by narrowing the types of some arguments;
• changes in the definiens which make it more convenient yet preserve the original meaning.

Redefinitions are heavily used in MML. in YELLOW_0 [5] as incarnations of analogous notions from ORDERS_1 [56] (see Section , p. ).

definition let A be non empty RelStr;
 redefine attr A is reflexive means                  :: YELLOW_0:def 1
    for x being Element of A holds x <= x;
end;

definition let A be RelStr;
 redefine
  attr A is transitive means                         :: YELLOW_0:def 2
    for x,y,z being Element of A st x <= y & y <= z holds x <= z;
 attr A is antisymmetric means                       :: YELLOW_0:def 3
    for x,y being Element of A st x <= y & y <= x holds x = y;
end;

YELLOW_0 also introduces a host of similar definitions which serve to bridge the state of MML and the requirements of formalizing the CCL-book. WAYBEL_0 [6] gives the final version of the concept of a lattice as

definition
 mode Semilattice is with_infima Poset;
 mode sup-Semilattice is with_suprema Poset;
 mode LATTICE is with_infima with_suprema Poset;
end;