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

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> 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.

I appreciate the helpful explanation -- thanks!  How can I determine
where in, say, FINSET_1, the registration FINSET_1:exreg 1 occurs, or
whether there even is such a thing?  Is there a command line tool for
finding out the answers to these questions?

Also, there are a bunch of applications like constr that are
distributed with mizar.  Where can I find documentation for these?

Thanks again,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*393: Incorrect beginning of a reasoning item