Interpretation of Locales in Isabelle:\\Managing Dependencies between Locales
Clemens Ballarin · 2006
Locales are the theory development modules of the Isabelle proof assistant. Interpretation is a powerful technique of theorem reuse which facilitates their automatic transport to other contexts. This paper is concerned with the interpretation of locales in the context of other locales. Our main concern is to make interpretation an effective tool in an interactive proof environment. Interpretation dependencies between locales are maintained explicitly, by means of a development graph, so that theorems proved in one locale can be propagated to other locales that interpret it. Proof tools in Isabelle are controlled by sets of default theorems they use. These sets are required to be finite, but can become infinite in the presence of arbitrary interpretations. We show that finiteness can be maintained.