[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Question about environments

Dear James,

On Thu, 7 Jan 2010, James Smith wrote:


I have a problem which boils down to the following:



begin

reserve n for Element of omega;
n is natural number;            :: This works because of the cluster...
                                ::
                                ::  -> natural Element of omega
                                ::
                                ::  ...in ORDINAL1, the coherence of which
is
                                ::  proved by ORDINAL1:def 13 (which
defines
                                ::  'natural' as meaning 'in omega',
essentially
                                ::  equivalent to 'Element of omega' with
the
                                ::  requirements SUBSET, BOOLE).

n in omega;                     :: Again this works because of the
requirements.


Exactly.


reserve k for natural number;

k in omega by ORDINAL1:def 13;  :: This works
k in omega;                     :: But this doesn't. Adding ORDINAL1 to the
                                ::  definitions directive makes no
difference.
The definition directive is mainly used to 'unfold' the definition when constructing proof skeletons (the other function is importing the explicite equalities defined with 'equals'). So it won't help to have the statement justified. 


I would like the assertion 'k in omega' to work without explicit reference
to the relevant definition. Is this possible?


Essentially the answer is 'no'.


Previously when I've come across what appear to be insurmountable problems
I've copied the offending lines to the end of existing MML articles and then
wittled down the environments, but when I copy and paste this assertion into
PYTHTRIP, for example, and try to verify it, I get the same *4 error. This
makes me suspect that the assertion can never be accepted without explicit
reference to the definition. Is this true?
The registration mechanism only that works on adjectives cannot be used to infer the 'in' predicate. It would, of course, be possible to build it into the requirements directive, but the gain is relatively small as references to ORDINAL1:def 13 are not so frequent. 

Best regards,

Adam

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================