[isabelle-dev] Data structures in HOL-Library

[Lukas Bulwahn]

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?



Lukas