Structured theories in LCF

An extension to the Edinburgh LCF interactive theorem-proving system is described which provides new ways of constructing theories, drawing upon ideas from the Clear specification language. A new theory can be built from an existing theory in two new ways: by renaming its types and constants, or by abstraction (forgetting some types and constants and perhaps renaming the rest). A way of providing parameterised theories is described. These theory-building operations — together with operations for forming a primitive theory and for taking the union of theories — allow large theories to be built in a flexible and well-structured fashion. Inference rules and strategies for proof in structured theories are also discussed.