[mizar] Functions between the positive real numbers?

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Mizar community,

I'm currently teaching a Mizar course, and a problem came up
that I haven't been able to solve.  Please help me with this.

I ask the students as an exercise to formalize the solution
of a puzzle from the international mathematical olympiads
that talks about a function from the positive real numbers
to the positive real numbers:

<http://www.cs.ru.nl/~freek/courses/pa-2007/exercises/exercise-mizar.pdf>

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.

So I have three (or in fact four, as one of the students
has tried two different approaches) attempts that I have
questions about.  But before bothering the list with these
files, maybe someone (Andrzej?) can just tell us how to
do this?  Or is not possible?

I would like to show my group how nice the Mizar type
system is (as it is!).  So not getting this to work is
frustrating...

Freek