6.7 Cluster Definition

We can make a type like new mode by giving some attribute to a certain mode. For example, suppose that there is mode called Real. Let us assume that the attribute of positive is defined to this mode. At this time, we can also make mode called "positive Real" (this is called cluster).
    Although it seems we are enough to make a new mode called positive_Real, convenience of cluster is as follows:

      x is positive_Real; then
      x is positive;

We can not derive the above, but we can derive the following without giving reason.

      x is positive Real; then
      x is positive;


That is, the Mizar checker remembers firmly that cluster called "positive Real" is positive Real. If once new cluster is defined, we can use the cluster freely in other articles by writing the first filename such as clusters of the environ section.
The example which defines cluster will be shown below. In the definition, let's keep in mind that it is necessary to prove only existence.
In addition, we will assume that the next is written in VOC file beforehand.

     Vpositive



   environ
     vocabulary TEST8;
     notation ARYTM,REAL_1;
     constructors ARYTM;
     theorems REAL_1,AXIOMS;
     requirements ARYTM;
    begin
     definition let x be Real;
        attr x is positive means　:A1: 0<x;
    end;
    definition
     cluster positive Real
     existence
     proof take 1; thus O<1; end;
    end;
    theorem for x,y begin positive Real
     holds x+y is positive Real
    proof let x,y is positive Real;
     B1:0くx by A1; then 0くy by A1; then
     x<x+y by REAL_1:69; then
     0<x+y by B1, AXIOMS:22;
    hence x+y is positive Real by A1;
    end: