Re: [isabelle] Non-determinism
On Thursday 07 September 2006 16:09, Gabriele Pozzani wrote:
> it's possible to do a non-deterministic assignment in Isabelle, or simulate
> Or, it's possible generate a random integer?
reflexivity is provable in Isabelle, i.e. "?x == ?x" is a theorem for any
?x -- in particular also for any term 'random ()', regardless of how you
define the function 'random'.
You can use 'arbitrary' for an arbitrary (but fixed) value of a given type, or
you can use the 'SOME' operator to define a constant which isn't fully
some_positive_int == SOME i::int. i > 0
Also see Section 5.2.6, "Definition by Specification", of the Isabelle/Isar
reference manual. Maybe we can give a more helpful answer if you let us know
what you want to do, i.e. in what context you want to model non-determinism.
This archive was generated by a fusion of
Pipermail (Mailman edition) and