Re: [isabelle] finite sets and code generation



Peter Gammie wrote:
> Hello,
>
> I am curious to know what the code generator can do with finite sets.
>
> For proof re-use reasons I use this idiom to fudge them into lists (in a definition context):
>
> xs_list = (SOME xs. set xs = { my finite set })
>
> The only substantial reason I have is that I can make use of the equivalence relation partition operator '_ // _' on these sets.
>   
When using SOME, you run into a fundamental problem: SOME makes a choice
that the
executable code cannot follow (as you can't tell anything about the
choice made).

One workaround is to parameterize over the SOME-operator, i.e. work
under the assumption that you have an operator that
behaves like SOME, but having the possibility to replace it by a
concrete one later.
However, I'm think this will not work without some manual refinement
steps from sets to lists (?)

Best,
  Peter

> Is there a way (does someone have some code) to partition lists? Is there a more-complete treatment of finite sets for the code generator somewhere?
>
> cheers
> peter
>
>   






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