Re: Inductive predicates

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

===============================================================
Grzegorz Bancerek
e-mail: [email protected] ([email protected])
http://merak.pb.bialystok.pl/~bancerek/
Dept. of Theoretical CS
Faculty of Computer Science      fax. +48 (85) 746-9057
Bialystok Technical University   tel. +48 (85) 746-9056
http://www.pb.bialystok.pl