20 % |
20 % |
21 \isamarkupchapter{Local theory specifications% |
21 \isamarkupchapter{Local theory specifications% |
22 } |
22 } |
23 \isamarkuptrue% |
23 \isamarkuptrue% |
24 % |
24 % |
|
25 \begin{isamarkuptext}% |
|
26 A \emph{local theory} combines aspects of both theory and proof |
|
27 context (cf.\ \secref{sec:context}), such that definitional |
|
28 specifications may be given relatively to parameters and |
|
29 assumptions. A local theory is represented as a regular proof |
|
30 context, augmented by administrative data about the \emph{target |
|
31 context}. |
|
32 |
|
33 The target is usually derived from the background theory by adding |
|
34 local \isa{{\isasymFIX}} and \isa{{\isasymASSUME}} elements, plus |
|
35 suitable modifications of non-logical context data (e.g.\ a special |
|
36 type-checking discipline). Once initialized, the target is ready to |
|
37 absorb definitional primitives: \isa{{\isasymDEFINE}} for terms and |
|
38 \isa{{\isasymNOTE}} for theorems. Such definitions may get |
|
39 transformed in a target-specific way, but the programming interface |
|
40 hides such details. |
|
41 |
|
42 Isabelle/Pure provides target mechanisms for locales, type-classes, |
|
43 type-class instantiations, and general overloading. In principle, |
|
44 users can implement new targets as well, but this rather arcane |
|
45 discipline is beyond the scope of this manual. In contrast, |
|
46 implementing derived definitional packages to be used within a local |
|
47 theory context is quite easy: the interfaces are even simpler and |
|
48 more abstract than the underlying primitives for raw theories. |
|
49 |
|
50 Many definitional packages for local theories are available in |
|
51 Isabelle. Although a few old packages only work for global |
|
52 theories, the local theory interface is already the standard way of |
|
53 implementing definitional packages in Isabelle.% |
|
54 \end{isamarkuptext}% |
|
55 \isamarkuptrue% |
|
56 % |
25 \isamarkupsection{Definitional elements% |
57 \isamarkupsection{Definitional elements% |
26 } |
58 } |
27 \isamarkuptrue% |
59 \isamarkuptrue% |
28 % |
60 % |
29 \begin{isamarkuptext}% |
61 \begin{isamarkuptext}% |
30 FIXME% |
62 There are separate elements \isa{{\isasymDEFINE}\ c\ {\isasymequiv}\ t} for terms, and |
31 \end{isamarkuptext}% |
63 \isa{{\isasymNOTE}\ b\ {\isacharequal}\ thm} for theorems. Types are treated |
32 \isamarkuptrue% |
64 implicitly, according to Hindley-Milner discipline (cf.\ |
|
65 \secref{sec:variables}). These definitional primitives essentially |
|
66 act like \isa{let}-bindings within a local context that may |
|
67 already contain earlier \isa{let}-bindings and some initial |
|
68 \isa{{\isasymlambda}}-bindings. Thus we gain \emph{dependent definitions} |
|
69 that are relative to an initial axiomatic context. The following |
|
70 diagram illustrates this idea of axiomatic elements versus |
|
71 definitional elements: |
|
72 |
|
73 \begin{center} |
|
74 \begin{tabular}{|l|l|l|} |
|
75 \hline |
|
76 & \isa{{\isasymlambda}}-binding & \isa{let}-binding \\ |
|
77 \hline |
|
78 types & fixed \isa{{\isasymalpha}} & arbitrary \isa{{\isasymbeta}} \\ |
|
79 terms & \isa{{\isasymFIX}\ x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} & \isa{{\isasymDEFINE}\ c\ {\isasymequiv}\ t} \\ |
|
80 theorems & \isa{{\isasymASSUME}\ a{\isacharcolon}\ A} & \isa{{\isasymNOTE}\ b\ {\isacharequal}\ \isactrlBG B\isactrlEN } \\ |
|
81 \hline |
|
82 \end{tabular} |
|
83 \end{center} |
|
84 |
|
85 A user package merely needs to produce suitable \isa{{\isasymDEFINE}} |
|
86 and \isa{{\isasymNOTE}} elements according to the application. For |
|
87 example, a package for inductive definitions might first \isa{{\isasymDEFINE}} a certain predicate as some fixed-point construction, |
|
88 then \isa{{\isasymNOTE}} a proven result about monotonicity of the |
|
89 functor involved here, and then produce further derived concepts via |
|
90 additional \isa{{\isasymDEFINE}} and \isa{{\isasymNOTE}} elements. |
|
91 |
|
92 The cumulative sequence of \isa{{\isasymDEFINE}} and \isa{{\isasymNOTE}} |
|
93 produced at package runtime is managed by the local theory |
|
94 infrastructure by means of an \emph{auxiliary context}. Thus the |
|
95 system holds up the impression of working within a fully abstract |
|
96 situation with hypothetical entities: \isa{{\isasymDEFINE}\ c\ {\isasymequiv}\ t} |
|
97 always results in a literal fact \isa{\isactrlBG c\ {\isasymequiv}\ t\isactrlEN }, where |
|
98 \isa{c} is a fixed variable \isa{c}. The details about |
|
99 global constants, name spaces etc. are handled internally. |
|
100 |
|
101 So the general structure of a local theory is a sandwich of three |
|
102 layers: |
|
103 |
|
104 \begin{center} |
|
105 \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}} |
|
106 \end{center} |
|
107 |
|
108 \noindent When a definitional package is finished, the auxiliary |
|
109 context is reset to the target context. The target now holds |
|
110 definitions for terms and theorems that stem from the hypothetical |
|
111 \isa{{\isasymDEFINE}} and \isa{{\isasymNOTE}} elements, transformed by |
|
112 the particular target policy (see |
|
113 \cite[\S4--5]{Haftmann-Wenzel:2009} for details).% |
|
114 \end{isamarkuptext}% |
|
115 \isamarkuptrue% |
|
116 % |
|
117 \isadelimmlref |
|
118 % |
|
119 \endisadelimmlref |
|
120 % |
|
121 \isatagmlref |
|
122 % |
|
123 \begin{isamarkuptext}% |
|
124 \begin{mldecls} |
|
125 \indexmltype{local\_theory}\verb|type local_theory = Proof.context| \\ |
|
126 \indexml{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex] |
|
127 \indexml{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline% |
|
128 \verb| (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline% |
|
129 \verb| (term * (string * thm)) * local_theory| \\ |
|
130 \indexml{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline% |
|
131 \verb| Attrib.binding * thm list -> local_theory ->|\isasep\isanewline% |
|
132 \verb| (string * thm list) * local_theory| \\ |
|
133 \end{mldecls} |
|
134 |
|
135 \begin{description} |
|
136 |
|
137 \item \verb|local_theory| represents local theories. Although |
|
138 this is merely an alias for \verb|Proof.context|, it is |
|
139 semantically a subtype of the same: a \verb|local_theory| holds |
|
140 target information as special context data. Subtyping means that |
|
141 any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used |
|
142 with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|. |
|
143 |
|
144 \item \verb|TheoryTarget.init|~\isa{NONE\ thy} initializes a |
|
145 trivial local theory from the given background theory. |
|
146 Alternatively, \isa{SOME\ name} may be given to initialize a |
|
147 \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified |
|
148 internal name is expected here). This is useful for experimentation |
|
149 --- normally the Isar toplevel already takes care to initialize the |
|
150 local theory context. |
|
151 |
|
152 \item \verb|LocalTheory.define|~\isa{kind\ {\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is |
|
153 given relatively to the current \isa{lthy} context. In |
|
154 particular the term of the RHS may refer to earlier local entities |
|
155 from the auxiliary context, or hypothetical parameters from the |
|
156 target context. The result is the newly defined term (which is |
|
157 always a fixed variable with exactly the same name as specified for |
|
158 the LHS), together with an equational theorem that states the |
|
159 definition as a hypothetical fact. |
|
160 |
|
161 Unless an explicit name binding is given for the RHS, the resulting |
|
162 fact will be called \isa{b{\isacharunderscore}def}. Any given attributes are |
|
163 applied to that same fact --- immediately in the auxiliary context |
|
164 \emph{and} in any transformed versions stemming from target-specific |
|
165 policies or any later interpretations of results from the target |
|
166 context (think of \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}, |
|
167 for example). This means that attributes should be usually plain |
|
168 declarations such as \hyperlink{attribute.simp}{\mbox{\isa{simp}}}, while non-trivial rules like |
|
169 \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}} are better avoided. |
|
170 |
|
171 The \isa{kind} determines the theorem kind tag of the resulting |
|
172 fact. Typical examples are \verb|Thm.definitionK|, \verb|Thm.theoremK|, or \verb|Thm.internalK|. |
|
173 |
|
174 \item \verb|LocalTheory.note|~\isa{kind\ {\isacharparenleft}a{\isacharcomma}\ ths{\isacharparenright}\ lthy} is |
|
175 analogous to \verb|LocalTheory.define|, but defines facts instead of |
|
176 terms. There is also a slightly more general variant \verb|LocalTheory.notes| that defines several facts (with attribute |
|
177 expressions) simultaneously. |
|
178 |
|
179 This is essentially the internal version of the \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} |
|
180 command, or \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} if an empty name binding is given. |
|
181 |
|
182 \end{description}% |
|
183 \end{isamarkuptext}% |
|
184 \isamarkuptrue% |
|
185 % |
|
186 \endisatagmlref |
|
187 {\isafoldmlref}% |
|
188 % |
|
189 \isadelimmlref |
|
190 % |
|
191 \endisadelimmlref |
33 % |
192 % |
34 \isamarkupsection{Morphisms and declarations% |
193 \isamarkupsection{Morphisms and declarations% |
35 } |
194 } |
36 \isamarkuptrue% |
195 \isamarkuptrue% |
37 % |
196 % |