Re: [mizar] Inductive predicates

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

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: bancerek@mizar.org (bancerek@math.uwb.edu.pl)
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