[isabelle-dev] Tech report: Simplifying automated data refinement via quotients

[Alexander Krauss]

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