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
> it?
> 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 
specified, e.g.

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