Re: [mizar] Nat not Real trouble

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

Hello,

On Tue, 24 Aug 2004 broderic@ugrad.cs.ualberta.ca wrote:

> Could someone explain to me why I get this error and how to work around it?

It seems that the whole thing is about a redefinition from SUBSET_1:

definition let D be non empty set, X be non empty Subset of D;
 redefine mode Element of X -> Element of D;
end;

It is used in the article NAT_1 which defines Nat (with the knowledge that
NAT is a non empty subset of REAL, and so Nat is exported to the database
as THIS 'Element of', not the original 'Element of' mode (SUBSET_1:def 2).
Clearly then,

>       consider n being Nat;
>       n is Real;

is accepted.

However, the original 'Element of' mode is used in FINSEQ_4:def 4 (the
definition of the restricted application), so the result type is 'only'
'Element of NAT', not 'Element of REAL', and

>     consider X being non empty set;
>     consider F being Function of X, NAT;
>     consider x being Element of X;
>       F/.x is Nat;
>       F/.x is Real;
> ::>              *4

is not accepted.

How to cope with it is a different story. Maybe just

reconsider Fx=F/.x as Nat;

and then

Fx is Real;

is accepted. I know it's not elegant, but at least it works.

Best,

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/
======================================================================