  In stepwise derivations of programs from specifications, data type
refinements are common. Many data type refinements involve isomorphic mappings
between the more abstract and more concrete data representations. Examples
include refinement of finite sets to duplicate-free ordered lists or to bit
vectors, adding record components that are functions of the other fields to
avoid expensive recomputation, etc. This paper describes the APT (Automated
Program Transformations) tools to carry out isomorphic data type refinements in
the ACL2 theorem prover and gives examples of their use. Because of the
inherent symmetry of isomorphisms, these tools are also useful to verify
existing programs, by turning more concrete data representations into more
abstract ones to ease verification. Typically, a data type will have relatively
few interface functions that access the internals of the type. Once versions of
these interface functions have been derived that work on the isomorphic type,
higher-level functions can be derived simply by substituting the old functions
for the new ones. We have implemented the APT transformations isodata to
generate the former, and propagate-iso for generating the latter functions as
well as theorems about the generated functions from the theorems about the
original functions. Propagate-iso also handles cases where the type is a
component of a more complex one such as a list of the type or a record that has
a field of the type: the isomorphism on the component type is automatically
lifted to an isomorphism on the more complex type. As with all APT
transformations, isodata and propagate-iso generate proofs of the relationship
of the transformed functions to the originals.
