Summary: The efficient implementation of abstract data types and all functions that manipulate them would permit application-oriented solutions to be developed without having to take undue account of executional properties. The synthesis of efficient concrete types and functions forms the basis of the present paper, which appeals to a theory of inverse functions for additional axioms to augment those of a first-order functional algebra. These axioms are then applied in the simplification of the combinator- expressions arising in the synthesis of the functions between the concrete types. We also show how the abstraction function itself may be deduced in certain situations where it is required to optimise particular operations on an abstract type. In addition to possessing rigorous mathematical foundations, the function-level axioms are more generally applicable than previous approaches to this problem, and induce a more mechanisable rewrite-based transformation system.