Re: [isabelle] What Isabelle maps to use to generate usual (ordered) maps

Hi Thomas,

I am wondering what is the map theory that I have to use in order to
usual ML maps: roughly trees ordered w.r.t. to keys?

This is still somewhat in flux, and there is no single best practice. You could

a) Use the red-black trees from HOL/Library/RBT.thy directly.

b) Use the mapping type defined in HOL/Library/Mapping. This is slightly more abstract, basically a copy of "'a => 'b option". In Isabelle2011, when you load RBT.thy, the code generator automatically uses red-black trees to implement mappings.

c) Use the Isabelle Collections Framework. See the ITP-10 paper by Peter Lammich and Andreas Lochbihler (

d) In the future, we hope that it will be possible to generate code from abstract types like "'a => 'b option" or "'a set" directly. But we're not quite there yet...

Hope this helps...

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