[isabelle-dev] Data structures in HOL-Library
bulwahn at in.tum.de
Thu Apr 21 14:05:31 CEST 2011
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
-- 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
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
More information about the isabelle-dev