Re: [mizar] Question about environments

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Hello,

thank you very much for your email.


On Thu, 7 Jan 2010, James Smith wrote:

> Good evening,
>
> I've been working on Mizar on and off for a couple of weeks now and I've
> made some progress with getting environments right, and learned a little
> about the MML library along the way. I've been trying to get the environment
> right for the PYTHTRIP article (I'm following Freek Wiedijk's tutorial) and
> I have a problem which boils down to the following:
>
> +++
>
> environ
>
> vocabularies ARYTM, ORDINAL2;
> notations SUBSET_1, ORDINAL1;
> constructors SUBSET_1, ORDINAL1;
> registrations ORDINAL1;
> theorems ORDINAL1;
> requirements SUBSET, BOOLE;
>
> 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.
>
> 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.
> ::>       *4
>
> +++
>
> I would like the assertion 'k in omega' to work without explicit reference
> to the relevant definition. Is this possible?



There is no way to have it working without explicit reference, but it's 
possible to introduce, so called, casting functor

definition
  let k be natural number;
  func Down(k) -> Element of omega equals
  k;
  coherence by ORDINAL1:def 13;
end;

and to use 'Down(k)' instead of 'k' whenever it is required.

Statements

Down(k) in omega;
Down(k) = k;

are obvious.

One more remark: in such cases I would rather use symbol 'NAT' instead of 
'omega'. 'NAT' is introduced in numbers.miz.


Best regards
Artur





> 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?
>
> Many thanks in advance for any help on this.
>
> Kind regards,
>
> James
>
> http://www.mygarble.com/


==========================================================================

Artur Kornilowicz                          e-mail: arturk@math.uwb.edu.pl

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Informatics                   tel. +48 (85) 745-7662
University of Bialystok                    fax. +48 (85) 745-7662
Sosnowa 64, 15-887 Bialystok, Poland