Re: [mizar] Type extensions

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

Freek Wiedijk wrote:

>  
>
> > Very similar problem apeared in the case of the type "Element of REAL"
> > and "Element of COMPLEX" (with the earlier not extending to the latter).
> >    
>
> Wasn't there a trick of redefining REAL to have a more
> specific type, "COMPLEX_set" say, and then redefining "Element
> of" when its argument is a COMPLEX_set to be a subtype of
> Element of COMPLEX?  I think something like that worked for me
> once.
>  

Now, with attributes, it may be a bit simpler:

definition let X be complex-membered set;
  redefine mode Element of X -> Element of COMPLEX;
 coherence;
end;

and with the registrations from 'MEMBERED' Mizar knows that
       REAL is complex-membered

> _If_ that works it's still very clumsy, of course.  Not something
> that you want.
>
>
>  
If 'Element of REAL' is identified according the redefinition above, the 
it is a new redefinitional variant and 'Element of NAT' does not widen 
to it!. One may introduce of course new 'Element of NAT' that widens to 
this 'Element of REAL' but then numerals will not be of the type 
'Element of NAT' (new one).

It is clumsy, indeed.

Regards,
Andrzej