RE: [mizar] Inductive predicates

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Dear Professor Andrzej Trybulec and All,

I wrote an evaluator for a functional language called SequenceL in Mizar. I have some recursive functions in my evaluator whose domains are very complicated so that their well-definedness proofs are too hard. I am thinking that writing them as recursive predicates and doing some proofs about those predicates would be much easier. That is why I wanted to start writing a recursive factorial as a recursive predicate as an exercise. I also wanted to see a definition from experts. I am hoping that I am on the right track.

Thanks and Regards,
Adem Ozyavas
________________________________________
From: owner-mizar-forum@mizar.uwb.edu.pl [owner-mizar-forum@mizar.uwb.edu.pl] On Behalf Of trybulec@math.uwb.edu.pl [trybulec@math.uwb.edu.pl]
Sent: Wednesday, September 02, 2009 3:58 AM
To: mizar-forum@mizar.uwb.edu.pl
Subject: RE: [mizar] 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" <adem.ozyavas@ttu.edu>:

> 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
>