Equality between Isabelle terms that use SOME

Question

I'm a little surprised that

value "let x = SOME n. n ∈ {1::int,2} in x = x"

returns True. After β-expanding and α-renaming, that term is the same as:

value "(SOME na. na ∈ {1::int,2}) = (SOME nb. nb ∈ {1::int,2})"

I don't see why this equality should hold. Why should the value chosen for na be the same as the value chosen for nb?

Answer 1

The term on the left hand side is exactly the same as the term on the right hand side (modulo alpha conversion). Therefore, they also have the same value. Equal (or rather alpha-equivalent) terms always produce equal values in HOL, since it is deterministic.

You can think of SOME x. P x giving you an arbitrary, but fixed value for which the property P holds (if such a value exists, otherwise just some arbitrary but fixed value about which you know nothing at all). In particular, different “calls” of SOME with the same argument will always give you the same value. The same is true of THE, undefined, and so on.

If you want true nondeterministic choice, you have to either use a different logic or model nondeterminism within HOL. The Refinement Framework offers a nondeterministic monad in which every operation can have zero, one, or many possible results.