Re: [isabelle] Non-determinism

Hello Gabriele,

It is not clear what you mean by doing an assignment in Isabelle. I assume you want to define a new constant without setting its actual value using an equality. There already exists an 'arbitrary' constant in Isabelle you can use for this :

term arbitrary;

Otherwise you can use definition by specification:

random :: nat

"random > 10 & random < 20"
apply arith

Here a new constant is defined with the property that is a nat in the range (10,20).

Hope I was on the right track,

On Thu, 7 Sep 2006, Gabriele Pozzani wrote:

Dear all,
it's possible to do a non-deterministic assignment in Isabelle, or simulate

Or, it's possible generate a random integer?

Thanks in advance for the collaboration.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.