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



Hi
> 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
>
>   
What's about
    d) Parameterize over choice-function (e.g. using a locale, fixing
choice and assuming: "s~={} ==> choice s : s"), do your definition
inside this locale
        and then instantiate to concrete set implementation ?

Best,
  Peter

> 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,
> 	Florian
>
>   






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