Email Gateway (Aug 18 2022 at 09:37): Email Gateway (Aug 18 2022 at 09:37):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
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
Email Gateway (Aug 18 2022 at 09:37):From: Tjark Weber <tjark.weber@gmx.de>
Gabriele,
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.
Best,
Tjark
Email Gateway (Aug 18 2022 at 09:37):From: Clemens Ballarin <ballarin@in.tum.de>
Randomness presumes a sequence of events that are being observed (and
the outcome of each individual event cannot be predicted). Doing this
formally can get pretty involved. Joe Hurd did a formalisation of
probability theory in HOL4.
I do not know which problem you are trying to solve, but normally
non-determinism is easiest modelled through a relation (or predicate).
That is, if your system can make the transitions a -> b and a -> c,
both (a, b) and (a, c) would be in the relation.
Clemens
Email Gateway (Aug 18 2022 at 09:37):From: Farhad Mehta <fmehta@inf.ethz.ch>
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.
Email Gateway (Aug 18 2022 at 09:38):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Thank you very much.
I seem to have resolved my problem (for the moment).
Gabriele
Last updated: Nov 21 2024 at 12:39 UTC