[Date Prev][Date Next] [Chronological] [Thread] [Top]

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