Re: [mizar] Re: a term representing the extension of a type

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

On Thu, 21 Dec 2006, Jesse Alama wrote:

> > ./constr -f 'text/myarticle' FRAENKEL:funcreg 1
> >
> > or so (try constr without arguments to see the invocation synopsis).
> Thanks!  When I ran this utility, I got the following:
>
> $ constr -f mizar/text/polyform.miz FRAENKEL:funcreg 1
> Required Constructors Directives, Mizar Ver. 7.8.03 (Darwin/FPC)
> Copyright (c) 1990-2006 Association of Mizar Users
>
> Constructors for FRAENKEL:funcreg 1 (with respect to mizar/text/polyform)
> FRAENKEL
>
> Once I added FRAENKEL to my the constructors directive, the error went
> away.
>
> By the way, what does `FRAENKEL:funcreg 1' mean?  And what does the
> invocation of constr on my file with the library reference
> `FRAENKEL:funcreg 1' mean?  (Sorry for asking such a basic question.
> I'm fraid I don't know of any source of documentation, apart from the
> people on this list, where I could look for an answer to my question.)
It's perfectly all right to ask this kind of question on mizar-forum - the 
usage of the 'constr' utility, and many others to be honest, is not 
documented very well, except for (sometimes cryptic) synopsis printed on 
invocation without parameters. But in the case of 'constr' it's not that 
bad after all - what one can see calling 'constr' without parameters is 
the following:
Required Constructors Directives, Mizar Ver. 7.8.03 (Linux/FPC)
Copyright (c) 1990-2006 Association of Mizar Users
Syntax:  constr [-f CheckingArticleFileName] <LibrRef>
where <LibrRef> is ArticleName[:[th|def|sch|exreg|funcreg|condreg] number]

Knowing that all the exported entities in the Mizar library depend on a 
certain set of constructors, we can query which ones these are - one can 
do this now with MMLQuery, but 'constr ' provides just the needed answer.
So one may call 'constr' to get the list of all constructors needed to 
understand (and so be able to import) _all_ items in a given article, e.g.
constr FRAENKEL

or ask only for constructors that are required by a certain item, e.g.

constr FRAENKEL:th 1

or ask only for the constructors as above which are not present in the 
environment of some article being prepared, e.g.
constr -f <somearticle> FRAENKEL

One point to note here is that in the case of theorems, definitions and 
schemes using 'constr' is easy - their numbering in abstracts can be used 
with the "th", "def" and "sch" markers, respectively. But in the case of 
registrations of attribute clusters, their three kinds (existential, 
functorial, and conditional) are numbered separately, and what is more, to 
ask a query with 'constr' the users must themselves count the 
registrations as their numbers are not included in abstracts (because 
normally one cannot refer to them in an article).
So any (existential) registration which registers the existence of a 
certain type with a set (cluster) of attributes like the following one 
from FRAENKEL can be addressed with 'exreg':
registration
 cluster non empty functional set;
end;

The registrations which register a set of attributes possessed by a 
certain instance of a functor can be addressed with 'funcreg' (functorial 
registrations), like this one:
registration let A, B be set;
 cluster Funcs(A,B) -> functional;
end;

And finally, conditional registration (where one set of attributes is 
proved to yield another set of attributes) can be addressed with 
'condreg':
registration let P be functional set;
 cluster -> Function-like Relation-like Element of P;
end;

The above conditional registration states that an empty set of attributes 
(no attributes listed before '->') yields the attributes 'Function-like' 
and 'Relation-like' for any object of type 'Element of P' where P is of 
type 'functional set'.
Sorry for bothering you with this longish explanation, but maybe some less 
experienced Mizar users can be saved some unnecessary work caused by the 
lack of better documentation.
Best regards,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================