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