Interpretation of Locales in Isabelle:\\Managing Dependencies between Locales

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.     «

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...     »