Re: [isabelle] finite sets and code generation
On 04/03/2010, at 8:21 PM, Daniel Wasserrab wrote:
> perhaps you might want to take a look at a publication from my colleague:
> Andreas Lochbihler: Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs 2009
> He describes how to generate code for finite functions in Isabelle and also gives an example for finite sets. This work is also accessible in the AFP: http://afp.sourceforge.net/entries/FinFun.shtml
Thanks for this! I am embarrassed that I didn't consult the AFP before sending that email
(Co)Incidentally this will at least solve another problem I was facing, viz dealing with functions over finite subsets of some arbitrary type, which may or may not coincide on the rest of the type... a problem I didn't expect to be so neatly treated as it is here.
Rene: thanks for your kind offer. I will see how Andreas's FinFuns work out.
This archive was generated by a fusion of
Pipermail (Mailman edition) and