Hi all, I recently looked into the code generation / data refinement situation again, to improve code generation for sets and functions. The general idea is to save the user from doing proofs using types Cset.set and friends, and instead provide automatic transport machinery to deal with specifications using sets directly.
I wrote a little tech report, which explains the ideas and most of the background. It is also a review of the existing implementations of transport machinery in Isabelle, notably the "transfer" tool and the quotient package. As these tools aren't very well known yet, this may be interesting to read even if you are not particularly interested in code generation. http://www4.in.tum.de/~krauss/papers/refinement.pdf A bit of material is still missing (e.g, the relationship to the Collections framework and a complete example). Nonetheless, feedback is very welcome already now. Cheers, Alex _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
