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

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

Hi,

Freek Wiedijk wrote:
> Then my question :-)  Suppose I define a functor like this:
>
>   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")

Following Josef suggestion (I suppose you're not a masochist)
you may write
  http://megrez.mizar.org/cgi-bin/emacs_search?entry=real_1:def+3
to get meaning of "REAL_1:def 3" which is introduced by "equals".
But it works only for submitted articles:-(
Anyway, Adam gave the meaning of your case:

>>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]};

>  (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 is possible to introduce in some cases schemes for convertion
Def->Th. But we need one scheme for any variant of loci and bounded
variable type in Fraenkel operator.

scheme Sch_args_bound {P[set,...,set], F(set,..,set) -> set}:
   for args,x holds x in foo(args) iff P[x,args]
provided
   for args holds F(args) = {x: P[x, args]};

When Fraenkel operator includes more complicated term with type
dependences between arguments
      { tau(args,bounds) where bounds: P[args, bounds]}
the conversion to Th (general statement) may be impossible.
But "fixed case" is possible

scheme Sch1_args_bounds {
   A1() -> type_1,
   ...,
   An() -> type_n of A1(), ..., An-1(),
   P[set,...,set], F(set,..,set) -> set}:
   for bounds,x holds
      x in foo(args) iff x = tau(A1(),...,An(),bounds) &
                         P[bounds, A1(), ..., An()]
provided
   for args holds F(args) = {tau(args,bounds): P[bounds, args]};

scheme Sch2_args_bound {
   A1() -> type_1,
   ...,
   An() -> type_n of A1(), ..., An-1(),
   P[set,...,set], F(set,..,set) -> set}:
   for bounds st P[bounds, A1(), ..., An()]
    holds  tau(A1(),...,An(),bounds) in F(args)
provided
   for args holds F(args) = {tau(args,bounds): P[bounds, args]};

It will be nice to have the schemes and theorems automatically.
However, I do not thing we should work on it
(such definition are rather rare and we need only
few steps to prove the correspoding theorem).

Best,
Grzegorz