[isabelle] Data structures in HOL-Library

Hi everyone,

in a private discussion with Andreas Lochbihler and Florian Haftmann, we have noticed that we should split the theories for data structures in HOL-Library (currently: RBT_Impl, RBT, AssocList, DList, CSet, Mapping) into more fine-grained theories.

If you require the implementation of one data structure, but you want to connect an abstract type with other data structure, the code equations must be manually deleted for one and added for the other because implementation and their connection to abstract type are within the same theory you would import from the Library.

Therefore, we propose the following naming scheme:

-- theories name of the representation types would end on "Impl", short for implementation.

-- theories that define the invariant-ensuring type and lift operations have no suffix in its theory name.

-- theories that connect the invariant-ensuring type and the abstract type are named by the scheme <invariant-ensuring type>_<abstract type>.

This would result in the following renamings:

for Red-Black trees: RBT_Impl remains RBT_Impl. RBT is split into RBT and RBT_Mapping.

for association lists: AssocList is split into AssocList_Impl and AssocList_Mapping. [AssocList is removed because AssocList has no invariant-ensuring type (yet).]

for distinct lists: DList is split into DList_Impl, DList, and DList_Cset.

for computable sets: Cset is split into Cset and List_Cset.

This way, the different layers are clearly separated in different theories.

For most users, this would mainly be noticed one would have to import, e.g., RBT_Mapping, instead of RBT to get executable Mappings based on red-black trees.

Any thoughts?


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