On Wed, 4 Apr 2007, Freek Wiedijk wrote:
> In the solution to this exercise, we would like to be able
> to use the notions from LIMFUNC1. So the simplest approach
> is just to use something like
>
> reserve f for PartFunc of REAL,REAL
>
> and then have conditions like
>
> for x being positive Real holds x in dom f
>
> and
>
> for x being positive Real holds f.x is positive Real
>
> That works. However, it is not very elegant.
>
> So both me and two of my students have tried to make
> redefinitions and clusters such that we could use
>
> reserve f for Function of posREAL,posREAL
>
> where
>
> posREAL -> Subset of REAL
>
> is the set of positive real numbers, and then -- because of
> those redefinitions/clusters -- have f _also_ automatically
> be of type "PartFunc of REAL,REAL". However, we have
> failed dismally. Worse, we got _very_ mystifying errors.
Apparently we've already discussed this problem (typical ;-)) - please see
the following archival thread and its follow-ups:
http://mizar.uwb.edu.pl/forum/archive/0609/msg00001.htmlBut I'm affraid no satisfying solution was offered then, and the library
and the system haven't changed yet to support the proposed "future"
solutions...
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@...
Sosnowa 64, 15-887 Bialystok, Poland
http://math.uwb.edu.pl/~adamn/======================================================================
