RE: Inductive predicates

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



> Hi,

> there is no regular recursive definition of predicates in Mizar.
> Instead you should use something like

> definition
> let X; let x,y be Element of X;
> pred x rec y means
> for Y st
>   (for a,b st START_CONDITION 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;

>Grzegorz

>On Sun, 16 Aug 2009, Ozyavas, Adem wrote:

> Dear All,
>
> Is there any way to write inductive predicates in Mizar?
>
> My purpose is to have inductive predicates instead of recursive functions to avoid existence and uniqueness proofs of recursive functions and leaving the fact that this predicate has functional property as a later task. I have searched the library and could not find any examples.
>
> Thanks...
>
> Adem Ozyavas