3.2.2 Notation Section and Constructors Section

In case of making a new theory, we sometimes want to use an old concept. For example, suppose that we want to use the concept of Function or Function-like. At this time, since these terms are registered into a vocabulary file called FUNC.VOC, we add FUNC to the vocabulary section. Moreover, since these terms are defined in FUNCT_1 (MIZ or ABS file), we add FUNCT-1 to the notation section. And in many cases, we add FUNCT_1 also to the constructors section.

Example;

       environ
          vocabulary FUNC;
          notation FUNCT_1;
          constructors FUNCT_1;
        begin
        reserve X for Function;
        theorem X is Function-like;



    About the difference between the notation section and the constructors section, there was only one item called the signature section in the version of old MIZAR and both were unified. From there, relations such as the hierarchic structure between concepts and the definition of each concept were expanded by the memory of a computer. However, since the former had many overlapping parts, it was separated for saving memory. The former was inserted into the constructors section. Therefore, when there was a file with more inclusive structure, we could omit the file of smaller structure from the constructors section, and it came to be able to perform saving of memory. For example, even if as follows instead of the previous example, an error does not come out.


        environ
        vocabulary FUNC;
      notation FUNCT_1;
      constructors TOPREAL1;


    begin
    reserve X for Function;
    theorem X is Function-like;



Therefore, when TOPREAL1 is contained in the constructors section beforehand, we don't have to insert FUNCT_1 there.
    At first, we can insert a file name into both the notation section and the constructors section in order, after completion, if a more basic file is deleted from the constructors section, we can simplify the environ section more, and we can also save memory.

    In the notation section, when we want to use symbols written in the files, we write the file names of articles that have those symbols defined. In the definition section (part of definition) of an article, those symbols' meanings are added (things like what kind of argument they have and how many, or what kind of modes they themselves become).

    For example, ∩(intersection) is defined in both of the articles BOOLE and PRE_TOPC (the latter is redefined). However, the method of using that symbol is different.

< article BOOLE >

definition
  let X,Y;
  func X /\ Y -> set means
  x c= it iff x in X & x in Y;
end;

< article PRE_TOPC >

definition
  let TP, P, Q;
  redefine
  func P /\ Q -> Subset of TP;
end;

   /\(same as ∩) in BOOLE means the set itself, and it has a set on the both sides as an argument. On the other hand, it in PRE_TOPC makes itself a Subset of TP(topological space), and it has Subsets of TP on both sides as an argument.
    From now on, when we want to write articles using /\, if we want to use that as a set, we write BOOLE in the notation section, and if we want it to be a Subset of TP, we have to write PRE_TOPC.