MML revisions

MML frequently undergoes revisions which change the articles already in it. Most changes are small but sometimes there are substantial modifications. A revision of the ``past'' is usually executed because with hindsight a better way is found to solve some problems. Here we would like to describe one such revision which was forced by the start of the CCL project, namely the modification of some MML contents to introduce a few basic lattice related notions. The other reason for spending some space in this paper on revisions is because of our conviction that revisions of the past will be unavoidable in any data base of formalized mathematics. Thus, such types of data bases should be furnished with a means for automating the process. However, we do not claim we have a solution to this problem--it is not as straightforward as it might appear at firsthand and many MML revisions are performed by hand.

Before the start of the CCL project, MML did not include a sufficiently general and flexible notion of a poset. In ORDERS_1 [56], a structure for posets was defined

definition
 struct poset (# 
   carrier -> non empty set,
   order -> Order of the carrier
 #)
end;

where Order of X is a reflexive, antisymmetric and transitive Relation of X. This structure was defined in 1990 and did not use the 1-sorted structure as a prefix since the latter was not introduced until 1995 in an MML revision.

The above structure is not flexible: the conditions for Order of are not split into the basic properties of reflexivity, transitivity, and antisymmetry. Therefore, should the need arise for a definition of a quasi-poset, for example, one would have to define another structure, develop its theory, and then make some sort of connection between an antisymmetric quasi-poset and a poset. This approach seemed to be a dead end if we ever planned to get to lattices.

A decision was made to revise ORDERS_1 and all articles depending on it by replacing the existing poset structure by a new, more general one which would allow for more convenient, object-oriented derivations. The definition of the poset structure was replaced by RelStr (see Section , p. ); the field order was replaced by InternalRel with a more general type Relation of the carrier. Attributes reflexive, antisymmetric, and transitive (previously defined to be applicable to a Relation) are now also defined for RelStr. In order to take advantage of MIZAR processing of these attributes, the following properties of functors were $\mathrm{registered}^{\:\alph{registrations}}$

definition let A be Poset;
  cluster the InternalRel of A -> Order-like;
end;

definition
  let X be set;
  let O be Order of X;
  cluster RelStr( #X, O #) -> reflexive transitive antisymmetric;
end;

Poset is then introduced as an expandable type (see Section , p. ).

Before the change of poset to Poset, four other articles covering theory of posets existed in MML and several other articles used some minor lemmas and notions from ORDERS_1. Of course, changes in ORDERS_1 influenced the correctness of these articles and some work was required to: update the environment sections of these articles, replace old notions by the new ones, and renumber theorems. Fortunately, many of these tasks could be done almost mechanically with a stream editor. Some simple generalizations of many facts were also made, but this work had to be done by hand.

The continuation of the CCL project prompted a number of other MML revisions--too technical to describe here.