Re: [isabelle] finite sets and code generation, once again

Hi Peter,

> One last question: I use SOME to choose an arbitrary element of a set. If I went all the way to lists I could implement it using hd.
> Is it easy to add such an operator to Fset?

executing choice is a difficult issue.  It largely depends on the
scenario.  Here a cursory sketch of approaches which I have thought of
until now how to resolve it:

a) Make choice irrelevant for generated code

c.f. src/HOL/ex/Execute_Choice.thy

b) Turn choice into definite choice

e.g. Min { ... } instead of SOME x \<in> { ... }

c) Turn specification non-deterministic using a set-monad

e.g. the pred type defined in src/HOL/Predicate.thy.  This means that
instead of using choice in an operation, the operation shall operate on
*all* suitable elements of a set, returning a set of results.  (I have
no example at hand because this is a fresh thought which has not yet
been explored further).

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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