1theory Examples1 2imports Examples 3begin 4 5section \<open>Use of Locales in Theories and Proofs 6 \label{sec:interpretation}\<close> 7 8text \<open> 9 Locales can be interpreted in the contexts of theories and 10 structured proofs. These interpretations are dynamic, too. 11 Conclusions of locales will be propagated to the current theory or 12 the current proof context.% 13\footnote{Strictly speaking, only interpretation in theories is 14 dynamic since it is not possible to change locales or the locale 15 hierarchy from within a proof.} 16 The focus of this section is on 17 interpretation in theories, but we will also encounter 18 interpretations in proofs, in 19 Section~\ref{sec:local-interpretation}. 20 21 As an example, consider the type of integers @{typ int}. The 22 relation @{term "(\<le>)"} is a total order over @{typ int}. We start 23 with the interpretation that @{term "(\<le>)"} is a partial order. The 24 facilities of the interpretation command are explored gradually in 25 three versions. 26\<close> 27 28 29subsection \<open>First Version: Replacement of Parameters Only 30 \label{sec:po-first}\<close> 31 32text \<open> 33 The command \isakeyword{interpretation} is for the interpretation of 34 locale in theories. In the following example, the parameter of locale 35 @{text partial_order} is replaced by @{term "(\<le>) :: int \<Rightarrow> int \<Rightarrow> 36 bool"} and the locale instance is interpreted in the current 37 theory.\<close> 38 39 interpretation %visible int: partial_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 40txt \<open>\normalsize 41 The argument of the command is a simple \emph{locale expression} 42 consisting of the name of the interpreted locale, which is 43 preceded by the qualifier @{text "int:"} and succeeded by a 44 white-space-separated list of terms, which provide a full 45 instantiation of the locale parameters. The parameters are referred 46 to by order of declaration, which is also the order in which 47 \isakeyword{print\_locale} outputs them. The locale has only a 48 single parameter, hence the list of instantiation terms is a 49 singleton. 50 51 The command creates the goal 52 @{subgoals [display]} which can be shown easily: 53\<close> 54 by unfold_locales auto 55 56text \<open>The effect of the command is that instances of all 57 conclusions of the locale are available in the theory, where names 58 are prefixed by the qualifier. For example, transitivity for @{typ 59 int} is named @{thm [source] int.trans} and is the following 60 theorem: 61 @{thm [display, indent=2] int.trans} 62 It is not possible to reference this theorem simply as @{text 63 trans}. This prevents unwanted hiding of existing theorems of the 64 theory by an interpretation.\<close> 65 66 67subsection \<open>Second Version: Replacement of Definitions\<close> 68 69text \<open>Not only does the above interpretation qualify theorem names. 70 The prefix @{text int} is applied to all names introduced in locale 71 conclusions including names introduced in definitions. The 72 qualified name @{text int.less} is short for 73 the interpretation of the definition, which is @{text "partial_order.less (\<le>)"}. 74 Qualified name and expanded form may be used almost 75 interchangeably.% 76\footnote{Since @{term "(\<le>)"} is polymorphic, for @{text "partial_order.less (\<le>)"} a 77 more general type will be inferred than for @{text int.less} which 78 is over type @{typ int}.} 79 The former is preferred on output, as for example in the theorem 80 @{thm [source] int.less_le_trans}: @{thm [display, indent=2] 81 int.less_le_trans} 82 Both notations for the strict order are not satisfactory. The 83 constant @{term "(<)"} is the strict order for @{typ int}. 84 In order to allow for the desired replacement, interpretation 85 accepts \emph{equations} in addition to the parameter instantiation. 86 These follow the locale expression and are indicated with the 87 keyword \isakeyword{rewrites}. This is the revised interpretation: 88\<close> 89end 90