Re: 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: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================