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:

consts
random :: nat

specification(random)
"random > 10 & random < 20"
apply arith
done

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,
Farhad.


On Thu, 7 Sep 2006, Gabriele Pozzani wrote:

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

Or, it's possible generate a random integer?

Thanks in advance for the collaboration.

Gabriele







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