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

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

Freek,

On Thu, 2 Jan 2003, Freek Wiedijk wrote:

>   definition
>    func foo args equals :Def: { x : P[x,args] };
>    ...
>   end;
>
> Then it would be nice to have as a theorem:
>
>   theorem Th: x in foo args iff P[x,args];
>
> But I just got the impression that putting "by Def" as a proof
> doesn't work!  So it's easy to put a more involved proof using Def.
> But I wonder now:
>
>  (a) what _is_ the statement "Def"? (clearly it's not "Th")

As far as I know, the definitional theorem associated with the 'equals'
type of definition in your case would be:

for args holds foo(args) = {x: P[x,args]};

In case of a functor definition of the form

definition
let x1 be T1, x2 be T2, ..., xn be Tn;
func foo(x1,x2,...,xn) -> T means definiens(it,x1,x2,...,xn);
end;

I believe, the definitional theorem is:

for IT being T, x1 being T1, x2 being T2, ..., xn being Tn holds
IT=foo(x1,x2,...,xn) iff definiens(IT,x1,x2,...,xn);

Maybe Dr Trybulec will want to comment on that, especially in view of
the recent discussion on automatic 'equals' expansion.

>  (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?

It would be nice, but I think there are no such schemes in the MML
at the moment. As we cannot write schemes with variable number of
arguments, it would be necessary to have many of them...

Adam Naumowicz