|
1 theory Examples1 |
|
2 imports Examples |
|
3 begin |
|
4 text {* \vspace{-5ex} *} |
|
5 section {* Use of Locales in Theories and Proofs |
|
6 \label{sec:interpretation} *} |
|
7 |
|
8 text {* |
|
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 "op \<le>"} is a total order over @{typ int}. We start |
|
23 with the interpretation that @{term "op \<le>"} is a partial order. The |
|
24 facilities of the interpretation command are explored gradually in |
|
25 three versions. |
|
26 *} |
|
27 |
|
28 |
|
29 subsection {* First Version: Replacement of Parameters Only |
|
30 \label{sec:po-first} *} |
|
31 |
|
32 text {* |
|
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 "op \<le> :: int \<Rightarrow> int \<Rightarrow> |
|
36 bool"} and the locale instance is interpreted in the current |
|
37 theory. *} |
|
38 |
|
39 interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" |
|
40 txt {* \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 *} |
|
54 by unfold_locales auto |
|
55 |
|
56 text {* 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. *} |
|
65 |
|
66 |
|
67 subsection {* Second Version: Replacement of Definitions *} |
|
68 |
|
69 text {* 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 @{term int.less}. |
|
74 Qualified name and expanded form may be used almost |
|
75 interchangeably.% |
|
76 \footnote{Since @{term "op \<le>"} is polymorphic, for @{term int.less} a |
|
77 more general type will be inferred than for @{text int.less} which |
|
78 is over type @{typ int}.} |
|
79 The latter 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 "op <"} 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{where}. This is the revised interpretation: |
|
88 *} |
|
89 end |