Re: [mizar] Scheme for func definition with Fraenkel operator?

[Adam Grabowski <adam@math.uwb.edu.pl>]

On Thu, 2 Jan 2003, Freek Wiedijk wrote:

> Then my question :-)  Suppose I define a functor like this:
>
>   definition
>    func foo args equals :Def: { x : P[x,args] };
>    ...
>   end;
>
>   theorem Th: x in foo args iff P[x,args];
>
>  (b) wouldn't it be nice to have a scheme "Sch" so that I would
>      be able to prove "Th" by just putting "... from Sch(Def);"
>
> So: does such a scheme already exist?  And if so, which one is it?
  What about schemes from LMOD_7 like Fr_1?

scheme Fr_1 {X() -> set, A() -> non empty set, a() -> Element of A(),
P[set]} :
 a() in X() iff P[a()]
provided
  X() = {a where a is Element of A() : P[a]};

with the proof of Th as follows:

Th: now let args;
A1:   foo args = { x : P[x, args] } by Def;
      let y;
      thus y in foo args iff P[y, args] from Fr_1 (A1);
    end;

  But this is not exactly the answer you need, I presume :)
  Adam