RE: Inductive predicates

You're right. The private constructors, like introduced by defpred, 
cannot be used in the exportable (public) part of the aricle. Just 
expand F and G in the
definition of the predicate.

Why you need such a predicate? The factorial is already define in MML:

NEWTON:def 2

Regards,
Andrzej Trybulec

Cytowanie "Ozyavas, Adem" <[email protected]>:

> Dear All,
>
> I asked Dr.Grzegorz Bancerek if there is inductive predicate 
> definitions in Mizar and below is Dr.Grzegorz Bancerek's answer.
> I tried to write the recursive definition of factorial using 
> Dr.Grzegorz Bancerek's
> template predicate definition.
> When I tried to define F and G functions "outside of predicate 
> definition" Mizar
> is complaining  that (I think all definitions are global) the 
> definition of pred is global and F and G are local as follows:
>
> deffunc F ...
> deffunc G ...
>
> definition
> let X; let x,y be Element of X;
> pred x fac y means :: x! = y
> for Y st
>   (for a,b st [a,b] = [0,1] holds [a,b] in Y) &
>   (for a,b st [a,b] in Y holds [F(a),G(b)] in Y)
> holds [x,y] in Y;
> end;
>
>
> How can one define the recursive factorial as predicate in Mizar with 
> F and G functions?
>
> Thank you...
>
> Adem Ozyavas
>