26869
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Spec}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
\isanewline
|
|
7 |
\isanewline
|
|
8 |
%
|
|
9 |
\endisadelimtheory
|
|
10 |
%
|
|
11 |
\isatagtheory
|
|
12 |
\isacommand{theory}\isamarkupfalse%
|
|
13 |
\ Spec\isanewline
|
|
14 |
\isakeyword{imports}\ Main\isanewline
|
|
15 |
\isakeyword{begin}%
|
|
16 |
\endisatagtheory
|
|
17 |
{\isafoldtheory}%
|
|
18 |
%
|
|
19 |
\isadelimtheory
|
|
20 |
%
|
|
21 |
\endisadelimtheory
|
|
22 |
%
|
27047
|
23 |
\isamarkupchapter{Theory specifications%
|
26869
|
24 |
}
|
|
25 |
\isamarkuptrue%
|
|
26 |
%
|
26870
|
27 |
\isamarkupsection{Defining theories \label{sec:begin-thy}%
|
|
28 |
}
|
|
29 |
\isamarkuptrue%
|
|
30 |
%
|
|
31 |
\begin{isamarkuptext}%
|
|
32 |
\begin{matharray}{rcl}
|
26902
|
33 |
\indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\
|
27042
|
34 |
\indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\
|
26870
|
35 |
\end{matharray}
|
|
36 |
|
27042
|
37 |
Isabelle/Isar theories are defined via theory file, which contain
|
|
38 |
both specifications and proofs; occasionally definitional mechanisms
|
|
39 |
also require some explicit proof. The theory body may be
|
|
40 |
sub-structered by means of \emph{local theory} target mechanisms,
|
|
41 |
notably \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}.
|
26870
|
42 |
|
26902
|
43 |
The first ``real'' command of any theory has to be \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which starts a new theory based on the merge of existing
|
|
44 |
ones. Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be
|
|
45 |
an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is relevant to
|
26870
|
46 |
document preparation only; it acts very much like a special
|
27052
|
47 |
pre-theory markup command (cf.\ \secref{sec:markup}). The \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command concludes a theory development; it has to be
|
|
48 |
the very last command of any theory file loaded in batch-mode.
|
26870
|
49 |
|
|
50 |
\begin{rail}
|
|
51 |
'theory' name 'imports' (name +) uses? 'begin'
|
|
52 |
;
|
|
53 |
|
|
54 |
uses: 'uses' ((name | parname) +);
|
|
55 |
\end{rail}
|
|
56 |
|
|
57 |
\begin{descr}
|
|
58 |
|
26902
|
59 |
\item [\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the
|
26870
|
60 |
merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
|
|
61 |
|
|
62 |
Due to inclusion of several ancestors, the overall theory structure
|
|
63 |
emerging in an Isabelle session forms a directed acyclic graph
|
|
64 |
(DAG). Isabelle's theory loader ensures that the sources
|
|
65 |
contributing to the development graph are always up-to-date.
|
|
66 |
Changed files are automatically reloaded when processing theory
|
|
67 |
headers.
|
|
68 |
|
26902
|
69 |
The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional
|
26870
|
70 |
dependencies on extra files (usually ML sources). Files will be
|
|
71 |
loaded immediately (as ML), unless the name is put in parentheses,
|
|
72 |
which merely documents the dependency to be resolved later in the
|
26902
|
73 |
text (typically via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} in the body text,
|
26870
|
74 |
see \secref{sec:ML}).
|
|
75 |
|
27042
|
76 |
\item [\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory
|
|
77 |
definition.
|
|
78 |
|
|
79 |
\end{descr}%
|
|
80 |
\end{isamarkuptext}%
|
|
81 |
\isamarkuptrue%
|
|
82 |
%
|
|
83 |
\isamarkupsection{Local theory targets \label{sec:target}%
|
|
84 |
}
|
|
85 |
\isamarkuptrue%
|
|
86 |
%
|
|
87 |
\begin{isamarkuptext}%
|
|
88 |
A local theory target is a context managed separately within the
|
|
89 |
enclosing theory. Contexts may introduce parameters (fixed
|
|
90 |
variables) and assumptions (hypotheses). Definitions and theorems
|
|
91 |
depending on the context may be added incrementally later on. Named
|
|
92 |
contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
|
|
93 |
(cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
|
|
94 |
global theory context.
|
|
95 |
|
|
96 |
\begin{matharray}{rcll}
|
|
97 |
\indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
98 |
\indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\
|
|
99 |
\end{matharray}
|
|
100 |
|
|
101 |
\indexouternonterm{target}
|
|
102 |
\begin{rail}
|
|
103 |
'context' name 'begin'
|
|
104 |
;
|
|
105 |
|
|
106 |
target: '(' 'in' name ')'
|
|
107 |
;
|
|
108 |
\end{rail}
|
|
109 |
|
|
110 |
\begin{descr}
|
|
111 |
|
|
112 |
\item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
|
|
113 |
existing locale or class context \isa{c}. Note that locale and
|
27052
|
114 |
class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as
|
|
115 |
well, in order to continue the local theory immediately after the
|
|
116 |
initial specification.
|
27042
|
117 |
|
|
118 |
\item [\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory
|
|
119 |
and continues the enclosing global theory. Note that a global
|
|
120 |
\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
|
|
121 |
theory itself (\secref{sec:begin-thy}).
|
|
122 |
|
|
123 |
\item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command
|
|
124 |
specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or
|
|
125 |
global theory context; the current target context will be suspended
|
|
126 |
for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
|
|
127 |
always produce a global result independently of the current target
|
|
128 |
context.
|
|
129 |
|
|
130 |
\end{descr}
|
|
131 |
|
|
132 |
The exact meaning of results produced within a local theory context
|
|
133 |
depends on the underlying target infrastructure (locale, type class
|
|
134 |
etc.). The general idea is as follows, considering a context named
|
|
135 |
\isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
|
|
136 |
|
|
137 |
Definitions are exported by introducing a global version with
|
|
138 |
additional arguments; a syntactic abbreviation links the long form
|
|
139 |
with the abstract version of the target context. For example,
|
|
140 |
\isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory
|
|
141 |
level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
|
|
142 |
abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
|
|
143 |
fixed parameter \isa{x}).
|
|
144 |
|
|
145 |
Theorems are exported by discharging the assumptions and
|
|
146 |
generalizing the parameters of the context. For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary
|
|
147 |
\isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
|
|
148 |
\end{isamarkuptext}%
|
|
149 |
\isamarkuptrue%
|
|
150 |
%
|
|
151 |
\isamarkupsection{Basic specification elements%
|
|
152 |
}
|
|
153 |
\isamarkuptrue%
|
|
154 |
%
|
|
155 |
\begin{isamarkuptext}%
|
|
156 |
\begin{matharray}{rcll}
|
|
157 |
\indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
|
|
158 |
\indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
159 |
\indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
|
|
160 |
\indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
161 |
\indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
162 |
\indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
163 |
\indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
164 |
\end{matharray}
|
|
165 |
|
|
166 |
These specification mechanisms provide a slightly more abstract view
|
|
167 |
than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see
|
|
168 |
\secref{sec:axms-thms}). In particular, type-inference is commonly
|
|
169 |
available, and result names need not be given.
|
|
170 |
|
|
171 |
\begin{rail}
|
|
172 |
'axiomatization' target? fixes? ('where' specs)?
|
|
173 |
;
|
|
174 |
'definition' target? (decl 'where')? thmdecl? prop
|
|
175 |
;
|
|
176 |
'abbreviation' target? mode? (decl 'where')? prop
|
|
177 |
;
|
|
178 |
('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
|
|
179 |
;
|
|
180 |
|
|
181 |
fixes: ((name ('::' type)? mixfix? | vars) + 'and')
|
|
182 |
;
|
|
183 |
specs: (thmdecl? props + 'and')
|
|
184 |
;
|
|
185 |
decl: name ('::' type)? mixfix?
|
|
186 |
;
|
|
187 |
\end{rail}
|
|
188 |
|
|
189 |
\begin{descr}
|
|
190 |
|
|
191 |
\item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants
|
|
192 |
simultaneously and states axiomatic properties for these. The
|
|
193 |
constants are marked as being specified once and for all, which
|
|
194 |
prevents additional specifications being issued later on.
|
|
195 |
|
|
196 |
Note that axiomatic specifications are only appropriate when
|
|
197 |
declaring a new logical system. Normal applications should only use
|
|
198 |
definitional mechanisms!
|
|
199 |
|
|
200 |
\item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
|
|
201 |
internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
|
|
202 |
given as \isa{eq}, which is then turned into a proven fact. The
|
|
203 |
given proposition may deviate from internal meta-level equality
|
|
204 |
according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
|
|
205 |
object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not
|
|
206 |
change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
|
|
207 |
|
|
208 |
Definitions may be presented with explicit arguments on the LHS, as
|
|
209 |
well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
|
|
210 |
\isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an
|
|
211 |
unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
|
|
212 |
|
|
213 |
\item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces
|
|
214 |
a syntactic constant which is associated with a certain term
|
|
215 |
according to the meta-level equality \isa{eq}.
|
|
216 |
|
|
217 |
Abbreviations participate in the usual type-inference process, but
|
|
218 |
are expanded before the logic ever sees them. Pretty printing of
|
|
219 |
terms involves higher-order rewriting with rules stemming from
|
|
220 |
reverted abbreviations. This needs some care to avoid overlapping
|
|
221 |
or looping syntactic replacements!
|
|
222 |
|
|
223 |
The optional \isa{mode} specification restricts output to a
|
|
224 |
particular print mode; using ``\isa{input}'' here achieves the
|
|
225 |
effect of one-way abbreviations. The mode may also include an
|
|
226 |
``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
|
|
227 |
declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
|
|
228 |
\secref{sec:syn-trans}.
|
|
229 |
|
|
230 |
\item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
|
|
231 |
of the current context.
|
|
232 |
|
|
233 |
\item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
|
|
234 |
syntax with an existing constant or fixed variable. This is a
|
|
235 |
robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
|
|
236 |
(\secref{sec:syn-trans}). Type declaration and internal syntactic
|
|
237 |
representation of the given entity is retrieved from the context.
|
|
238 |
|
|
239 |
\item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the
|
|
240 |
present context.
|
|
241 |
|
|
242 |
\end{descr}
|
|
243 |
|
|
244 |
All of these specifications support local theory targets (cf.\
|
|
245 |
\secref{sec:target}).%
|
|
246 |
\end{isamarkuptext}%
|
|
247 |
\isamarkuptrue%
|
|
248 |
%
|
|
249 |
\isamarkupsection{Generic declarations%
|
|
250 |
}
|
|
251 |
\isamarkuptrue%
|
|
252 |
%
|
|
253 |
\begin{isamarkuptext}%
|
|
254 |
Arbitrary operations on the background context may be wrapped-up as
|
|
255 |
generic declaration elements. Since the underlying concept of local
|
|
256 |
theories may be subject to later re-interpretation, there is an
|
|
257 |
additional dependency on a morphism that tells the difference of the
|
|
258 |
original declaration context wrt.\ the application context
|
|
259 |
encountered later on. A fact declaration is an important special
|
|
260 |
case: it consists of a theorem which is applied to the context by
|
|
261 |
means of an attribute.
|
|
262 |
|
|
263 |
\begin{matharray}{rcl}
|
|
264 |
\indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
265 |
\indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
|
266 |
\end{matharray}
|
|
267 |
|
|
268 |
\begin{rail}
|
|
269 |
'declaration' target? text
|
|
270 |
;
|
|
271 |
'declare' target? (thmrefs + 'and')
|
|
272 |
;
|
|
273 |
\end{rail}
|
|
274 |
|
|
275 |
\begin{descr}
|
|
276 |
|
|
277 |
\item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration
|
|
278 |
function \isa{d} of ML type \verb|declaration|, to the current
|
|
279 |
local theory under construction. In later application contexts, the
|
|
280 |
function is transformed according to the morphisms being involved in
|
|
281 |
the interpretation hierarchy.
|
|
282 |
|
|
283 |
\item [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the
|
|
284 |
current local theory context. No theorem binding is involved here,
|
|
285 |
unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
|
|
286 |
\secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
|
|
287 |
of applying attributes as included in the theorem specification.
|
|
288 |
|
|
289 |
\end{descr}%
|
|
290 |
\end{isamarkuptext}%
|
|
291 |
\isamarkuptrue%
|
|
292 |
%
|
|
293 |
\isamarkupsection{Locales \label{sec:locale}%
|
|
294 |
}
|
|
295 |
\isamarkuptrue%
|
|
296 |
%
|
|
297 |
\begin{isamarkuptext}%
|
|
298 |
Locales are named local contexts, consisting of a list of
|
|
299 |
declaration elements that are modeled after the Isar proof context
|
|
300 |
commands (cf.\ \secref{sec:proof-context}).%
|
|
301 |
\end{isamarkuptext}%
|
|
302 |
\isamarkuptrue%
|
|
303 |
%
|
|
304 |
\isamarkupsubsection{Locale specifications%
|
|
305 |
}
|
|
306 |
\isamarkuptrue%
|
|
307 |
%
|
|
308 |
\begin{isamarkuptext}%
|
|
309 |
\begin{matharray}{rcl}
|
|
310 |
\indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
311 |
\indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
312 |
\indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
313 |
\indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
|
|
314 |
\indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
|
|
315 |
\end{matharray}
|
|
316 |
|
|
317 |
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
|
|
318 |
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
|
|
319 |
\indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
|
|
320 |
\begin{rail}
|
|
321 |
'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
|
|
322 |
;
|
|
323 |
'print\_locale' '!'? localeexpr
|
|
324 |
;
|
|
325 |
localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
|
|
326 |
;
|
|
327 |
|
|
328 |
contextexpr: nameref | '(' contextexpr ')' |
|
|
329 |
(contextexpr (name mixfix? +)) | (contextexpr + '+')
|
|
330 |
;
|
|
331 |
contextelem: fixes | constrains | assumes | defines | notes
|
|
332 |
;
|
|
333 |
fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
|
|
334 |
;
|
|
335 |
constrains: 'constrains' (name '::' type + 'and')
|
|
336 |
;
|
|
337 |
assumes: 'assumes' (thmdecl? props + 'and')
|
|
338 |
;
|
|
339 |
defines: 'defines' (thmdecl? prop proppat? + 'and')
|
|
340 |
;
|
|
341 |
notes: 'notes' (thmdef? thmrefs + 'and')
|
|
342 |
;
|
|
343 |
includes: 'includes' contextexpr
|
|
344 |
;
|
|
345 |
\end{rail}
|
|
346 |
|
|
347 |
\begin{descr}
|
|
348 |
|
|
349 |
\item [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] defines a
|
|
350 |
new locale \isa{loc} as a context consisting of a certain view of
|
|
351 |
existing locales (\isa{import}) plus some additional elements
|
|
352 |
(\isa{body}). Both \isa{import} and \isa{body} are optional;
|
|
353 |
the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
|
|
354 |
locale, which may still be useful to collect declarations of facts
|
|
355 |
later on. Type-inference on locale expressions automatically takes
|
|
356 |
care of the most general typing that the combined context elements
|
|
357 |
may acquire.
|
|
358 |
|
|
359 |
The \isa{import} consists of a structured context expression,
|
|
360 |
consisting of references to existing locales, renamed contexts, or
|
|
361 |
merged contexts. Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
|
|
362 |
parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
|
|
363 |
position. Renaming by default deletes concrete syntax, but new
|
|
364 |
syntax may by specified with a mixfix annotation. An exeption of
|
|
365 |
this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
|
|
366 |
be changed. Merging proceeds from left-to-right, suppressing any
|
|
367 |
duplicates stemming from different paths through the import
|
|
368 |
hierarchy.
|
|
369 |
|
|
370 |
The \isa{body} consists of basic context elements, further context
|
|
371 |
expressions may be included as well.
|
|
372 |
|
|
373 |
\begin{descr}
|
|
374 |
|
|
375 |
\item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local
|
|
376 |
parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
|
|
377 |
are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
|
|
378 |
implicitly in this context.
|
|
379 |
|
|
380 |
\item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type
|
|
381 |
constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
|
|
382 |
|
|
383 |
\item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}]
|
|
384 |
introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
|
|
385 |
proof (cf.\ \secref{sec:proof-context}).
|
|
386 |
|
|
387 |
\item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously
|
|
388 |
declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
|
|
389 |
proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
|
|
390 |
takes an equational proposition instead of variable-term pair. The
|
|
391 |
left-hand side of the equation may have additional arguments, e.g.\
|
|
392 |
``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
|
|
393 |
|
|
394 |
\item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
|
|
395 |
reconsiders facts within a local context. Most notably, this may
|
|
396 |
include arbitrary declarations in any attribute specifications
|
|
397 |
included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
|
|
398 |
|
|
399 |
\item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
|
|
400 |
in a statically scoped manner. Only available in the long goal
|
|
401 |
format of \secref{sec:goals}.
|
|
402 |
|
|
403 |
In contrast, the initial \isa{import} specification of a locale
|
|
404 |
expression maintains a dynamic relation to the locales being
|
|
405 |
referenced (benefiting from any later fact declarations in the
|
|
406 |
obvious manner).
|
|
407 |
|
|
408 |
\end{descr}
|
|
409 |
|
|
410 |
Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
|
|
411 |
in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
|
|
412 |
are illegal in locale definitions. In the long goal format of
|
|
413 |
\secref{sec:goals}, term bindings may be included as expected,
|
|
414 |
though.
|
|
415 |
|
|
416 |
\medskip By default, locale specifications are ``closed up'' by
|
|
417 |
turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
|
|
418 |
(modulo local definitions). The predicate statement covers only the
|
|
419 |
newly specified assumptions, omitting the content of included locale
|
|
420 |
expressions. The full cumulative view is only provided on export,
|
|
421 |
involving another predicate \isa{loc} that refers to the complete
|
|
422 |
specification text.
|
|
423 |
|
|
424 |
In any case, the predicate arguments are those locale parameters
|
|
425 |
that actually occur in the respective piece of text. Also note that
|
|
426 |
these predicates operate at the meta-level in theory, but the locale
|
|
427 |
packages attempts to internalize statements according to the
|
|
428 |
object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
|
|
429 |
\isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
|
|
430 |
\secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
|
|
431 |
|
|
432 |
The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
|
|
433 |
the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
|
|
434 |
constructions. Predicates are also omitted for empty specification
|
|
435 |
texts.
|
|
436 |
|
|
437 |
\item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
|
|
438 |
specified locale expression in a flattened form. The notable
|
|
439 |
special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
|
|
440 |
contents of the named locale, but keep in mind that type-inference
|
|
441 |
will normalize type variables according to the usual alphabetical
|
|
442 |
order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
|
|
443 |
Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
|
|
444 |
|
|
445 |
\item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
|
|
446 |
of the current theory.
|
|
447 |
|
|
448 |
\item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
|
|
449 |
repeatedly expand all introduction rules of locale predicates of the
|
|
450 |
theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
|
|
451 |
assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
|
|
452 |
\isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
|
|
453 |
specifications entailed by the context, both from target and
|
|
454 |
\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
|
|
455 |
below). New goals that are entailed by the current context are
|
|
456 |
discharged automatically.
|
|
457 |
|
|
458 |
\end{descr}%
|
|
459 |
\end{isamarkuptext}%
|
|
460 |
\isamarkuptrue%
|
|
461 |
%
|
|
462 |
\isamarkupsubsection{Interpretation of locales%
|
|
463 |
}
|
|
464 |
\isamarkuptrue%
|
|
465 |
%
|
|
466 |
\begin{isamarkuptext}%
|
|
467 |
Locale expressions (more precisely, \emph{context expressions}) may
|
|
468 |
be instantiated, and the instantiated facts added to the current
|
|
469 |
context. This requires a proof of the instantiated specification
|
|
470 |
and is called \emph{locale interpretation}. Interpretation is
|
|
471 |
possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
|
|
472 |
|
|
473 |
\begin{matharray}{rcl}
|
|
474 |
\indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\
|
|
475 |
\indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
|
|
476 |
\indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
477 |
\end{matharray}
|
|
478 |
|
|
479 |
\indexouternonterm{interp}
|
|
480 |
\begin{rail}
|
|
481 |
'interpretation' (interp | name ('<' | subseteq) contextexpr)
|
|
482 |
;
|
|
483 |
'interpret' interp
|
|
484 |
;
|
|
485 |
'print\_interps' '!'? name
|
|
486 |
;
|
|
487 |
instantiation: ('[' (inst+) ']')?
|
|
488 |
;
|
|
489 |
interp: thmdecl? \\ (contextexpr instantiation |
|
|
490 |
name instantiation 'where' (thmdecl? prop + 'and'))
|
|
491 |
;
|
|
492 |
\end{rail}
|
|
493 |
|
|
494 |
\begin{descr}
|
|
495 |
|
|
496 |
\item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
|
|
497 |
|
|
498 |
The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms
|
|
499 |
\isa{insts} and is positional. All parameters must receive an
|
|
500 |
instantiation term --- with the exception of defined parameters.
|
|
501 |
These are, if omitted, derived from the defining equation and other
|
|
502 |
instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
|
|
503 |
|
|
504 |
The command generates proof obligations for the instantiated
|
|
505 |
specifications (assumes and defines elements). Once these are
|
|
506 |
discharged by the user, instantiated facts are added to the theory
|
|
507 |
in a post-processing phase.
|
|
508 |
|
|
509 |
Additional equations, which are unfolded in facts during
|
|
510 |
post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
|
|
511 |
This is useful for interpreting concepts introduced through
|
|
512 |
definition specification elements. The equations must be proved.
|
|
513 |
Note that if equations are present, the context expression is
|
|
514 |
restricted to a locale name.
|
|
515 |
|
|
516 |
The command is aware of interpretations already active in the
|
|
517 |
theory. No proof obligations are generated for those, neither is
|
|
518 |
post-processing applied to their facts. This avoids duplication of
|
|
519 |
interpreted facts, in particular. Note that, in the case of a
|
|
520 |
locale with import, parts of the interpretation may already be
|
|
521 |
active. The command will only generate proof obligations and
|
|
522 |
process facts for new parts.
|
|
523 |
|
|
524 |
The context expression may be preceded by a name and/or attributes.
|
|
525 |
These take effect in the post-processing of facts. The name is used
|
|
526 |
to prefix fact names, for example to avoid accidental hiding of
|
|
527 |
other facts. Attributes are applied after attributes of the
|
|
528 |
interpreted facts.
|
|
529 |
|
|
530 |
Adding facts to locales has the effect of adding interpreted facts
|
|
531 |
to the theory for all active interpretations also. That is,
|
|
532 |
interpretations dynamically participate in any facts added to
|
|
533 |
locales.
|
|
534 |
|
|
535 |
\item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]
|
|
536 |
|
|
537 |
This form of the command interprets \isa{expr} in the locale
|
|
538 |
\isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the
|
|
539 |
localized version of the theorem command, the proof is in the
|
|
540 |
context of \isa{name}. After the proof obligation has been
|
|
541 |
dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
|
|
542 |
context \isa{name} is subsequently entered. Note that, like
|
|
543 |
import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
|
|
544 |
Like facts of renamed context elements, facts obtained by
|
|
545 |
interpretation may be accessed by prefixing with the parameter
|
|
546 |
renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
|
|
547 |
|
|
548 |
Unlike interpretation in theories, instantiation is confined to the
|
|
549 |
renaming of parameters, which may be specified as part of the
|
|
550 |
context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
|
|
551 |
|
|
552 |
Only specification fragments of \isa{expr} that are not already
|
|
553 |
part of \isa{name} (be it imported, derived or a derived fragment
|
|
554 |
of the import) are considered by interpretation. This enables
|
|
555 |
circular interpretations.
|
|
556 |
|
|
557 |
If interpretations of \isa{name} exist in the current theory, the
|
|
558 |
command adds interpretations for \isa{expr} as well, with the same
|
|
559 |
prefix and attributes, although only for fragments of \isa{expr}
|
|
560 |
that are not interpreted in the theory already.
|
|
561 |
|
|
562 |
\item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
|
|
563 |
interprets \isa{expr} in the proof context and is otherwise
|
|
564 |
similar to interpretation in theories.
|
|
565 |
|
|
566 |
\item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
|
|
567 |
interpretations of a particular locale \isa{loc} that are active
|
|
568 |
in the current context, either theory or proof context. The
|
|
569 |
exclamation point argument triggers printing of \emph{witness}
|
|
570 |
theorems justifying interpretations. These are normally omitted
|
|
571 |
from the output.
|
|
572 |
|
|
573 |
\end{descr}
|
|
574 |
|
|
575 |
\begin{warn}
|
|
576 |
Since attributes are applied to interpreted theorems,
|
|
577 |
interpretation may modify the context of common proof tools, e.g.\
|
|
578 |
the Simplifier or Classical Reasoner. Since the behavior of such
|
|
579 |
automated reasoning tools is \emph{not} stable under
|
|
580 |
interpretation morphisms, manual declarations might have to be
|
|
581 |
issued.
|
|
582 |
\end{warn}
|
|
583 |
|
|
584 |
\begin{warn}
|
|
585 |
An interpretation in a theory may subsume previous
|
|
586 |
interpretations. This happens if the same specification fragment
|
|
587 |
is interpreted twice and the instantiation of the second
|
|
588 |
interpretation is more general than the interpretation of the
|
|
589 |
first. A warning is issued, since it is likely that these could
|
|
590 |
have been generalized in the first place. The locale package does
|
|
591 |
not attempt to remove subsumed interpretations.
|
|
592 |
\end{warn}%
|
|
593 |
\end{isamarkuptext}%
|
|
594 |
\isamarkuptrue%
|
|
595 |
%
|
|
596 |
\isamarkupsection{Classes \label{sec:class}%
|
|
597 |
}
|
|
598 |
\isamarkuptrue%
|
|
599 |
%
|
|
600 |
\begin{isamarkuptext}%
|
|
601 |
A class is a particular locale with \emph{exactly one} type variable
|
|
602 |
\isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
|
|
603 |
is established which is interpreted logically as axiomatic type
|
|
604 |
class \cite{Wenzel:1997:TPHOL} whose logical content are the
|
|
605 |
assumptions of the locale. Thus, classes provide the full
|
|
606 |
generality of locales combined with the commodity of type classes
|
|
607 |
(notably type-inference). See \cite{isabelle-classes} for a short
|
|
608 |
tutorial.
|
|
609 |
|
|
610 |
\begin{matharray}{rcl}
|
|
611 |
\indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
612 |
\indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
613 |
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
|
|
614 |
\indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
|
|
615 |
\indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
616 |
\indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
|
|
617 |
\end{matharray}
|
|
618 |
|
|
619 |
\begin{rail}
|
|
620 |
'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
|
|
621 |
'begin'?
|
|
622 |
;
|
|
623 |
'instantiation' (nameref + 'and') '::' arity 'begin'
|
|
624 |
;
|
|
625 |
'instance'
|
|
626 |
;
|
|
627 |
'subclass' target? nameref
|
|
628 |
;
|
|
629 |
'print\_classes'
|
|
630 |
;
|
|
631 |
|
|
632 |
superclassexpr: nameref | (nameref '+' superclassexpr)
|
|
633 |
;
|
|
634 |
\end{rail}
|
|
635 |
|
|
636 |
\begin{descr}
|
|
637 |
|
|
638 |
\item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines
|
|
639 |
a new class \isa{c}, inheriting from \isa{superclasses}. This
|
|
640 |
introduces a locale \isa{c} with import of all locales \isa{superclasses}.
|
|
641 |
|
|
642 |
Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
|
|
643 |
theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter
|
|
644 |
\isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
|
|
645 |
|
|
646 |
Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
|
|
647 |
mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
|
|
648 |
corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
|
|
649 |
corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
|
|
650 |
--- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
|
|
651 |
class membership proofs.
|
|
652 |
|
|
653 |
\item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\
|
|
654 |
\secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the
|
|
655 |
particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
|
|
656 |
in the target body poses a goal stating these type arities. The
|
|
657 |
target is concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
|
|
658 |
|
|
659 |
Note that a list of simultaneous type constructors may be given;
|
|
660 |
this corresponds nicely to mutual recursive type definitions, e.g.\
|
|
661 |
in Isabelle/HOL.
|
|
662 |
|
|
663 |
\item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets
|
|
664 |
up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
|
|
665 |
the type classes involved. After finishing the proof, the
|
|
666 |
background theory will be augmented by the proven type arities.
|
|
667 |
|
|
668 |
\item [\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c}] in a class context for class
|
|
669 |
\isa{d} sets up a goal stating that class \isa{c} is logically
|
|
670 |
contained in class \isa{d}. After finishing the proof, class
|
|
671 |
\isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
|
|
672 |
|
|
673 |
\item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
|
|
674 |
theory.
|
|
675 |
|
|
676 |
\item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
|
|
677 |
introduction rules of this theory. Note that this method usually
|
|
678 |
needs not be named explicitly, as it is already included in the
|
|
679 |
default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
|
|
680 |
instantiation of trivial (syntactic) classes may be performed by a
|
|
681 |
single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
|
26870
|
682 |
|
|
683 |
\end{descr}%
|
|
684 |
\end{isamarkuptext}%
|
|
685 |
\isamarkuptrue%
|
|
686 |
%
|
27042
|
687 |
\isamarkupsubsection{The class target%
|
|
688 |
}
|
|
689 |
\isamarkuptrue%
|
|
690 |
%
|
|
691 |
\begin{isamarkuptext}%
|
|
692 |
%FIXME check
|
|
693 |
|
|
694 |
A named context may refer to a locale (cf.\ \secref{sec:target}).
|
|
695 |
If this locale is also a class \isa{c}, apart from the common
|
|
696 |
locale target behaviour the following happens.
|
|
697 |
|
|
698 |
\begin{itemize}
|
|
699 |
|
|
700 |
\item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
|
|
701 |
local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
|
|
702 |
are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
|
|
703 |
referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
|
|
704 |
|
|
705 |
\item Local theorem bindings are lifted as are assumptions.
|
|
706 |
|
|
707 |
\item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
|
|
708 |
global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
|
|
709 |
resolves ambiguities. In rare cases, manual type annotations are
|
|
710 |
needed.
|
|
711 |
|
|
712 |
\end{itemize}%
|
|
713 |
\end{isamarkuptext}%
|
|
714 |
\isamarkuptrue%
|
|
715 |
%
|
27054
|
716 |
\isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
|
27042
|
717 |
}
|
|
718 |
\isamarkuptrue%
|
|
719 |
%
|
|
720 |
\begin{isamarkuptext}%
|
27054
|
721 |
\begin{matharray}{rcl}
|
27042
|
722 |
\indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
|
|
723 |
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
|
|
724 |
\end{matharray}
|
|
725 |
|
|
726 |
Axiomatic type classes are Isabelle/Pure's primitive
|
|
727 |
\emph{definitional} interface to type classes. For practical
|
|
728 |
applications, you should consider using classes
|
|
729 |
(cf.~\secref{sec:classes}) which provide high level interface.
|
|
730 |
|
|
731 |
\begin{rail}
|
|
732 |
'axclass' classdecl (axmdecl prop +)
|
|
733 |
;
|
|
734 |
'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
|
|
735 |
;
|
|
736 |
\end{rail}
|
|
737 |
|
|
738 |
\begin{descr}
|
|
739 |
|
|
740 |
\item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of
|
|
741 |
existing classes, with additional axioms holding. Class axioms may
|
|
742 |
not contain more than one type variable. The class axioms (with
|
|
743 |
implicit sort constraints added) are bound to the given names.
|
|
744 |
Furthermore a class introduction rule is generated (being bound as
|
|
745 |
\isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
|
|
746 |
|
|
747 |
The ``class axioms'' are stored as theorems according to the given
|
|
748 |
name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
|
|
749 |
the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
|
|
750 |
|
|
751 |
\item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
|
|
752 |
\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}]
|
|
753 |
setup a goal stating a class relation or type arity. The proof
|
|
754 |
would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
|
|
755 |
the characteristic theorems of the type classes involved. After
|
|
756 |
finishing the proof, the theory will be augmented by a type
|
|
757 |
signature declaration corresponding to the resulting theorem.
|
|
758 |
|
|
759 |
\end{descr}%
|
|
760 |
\end{isamarkuptext}%
|
|
761 |
\isamarkuptrue%
|
|
762 |
%
|
|
763 |
\isamarkupsection{Unrestricted overloading%
|
|
764 |
}
|
|
765 |
\isamarkuptrue%
|
|
766 |
%
|
|
767 |
\begin{isamarkuptext}%
|
|
768 |
Isabelle/Pure's definitional schemes support certain forms of
|
|
769 |
overloading (see \secref{sec:consts}). At most occassions
|
|
770 |
overloading will be used in a Haskell-like fashion together with
|
|
771 |
type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
|
|
772 |
\secref{sec:class}). Sometimes low-level overloading is desirable.
|
|
773 |
The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
|
|
774 |
end-users.
|
|
775 |
|
|
776 |
\begin{matharray}{rcl}
|
|
777 |
\indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
|
|
778 |
\end{matharray}
|
|
779 |
|
|
780 |
\begin{rail}
|
|
781 |
'overloading' \\
|
|
782 |
( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
|
|
783 |
\end{rail}
|
|
784 |
|
|
785 |
\begin{descr}
|
|
786 |
|
|
787 |
\item [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}]
|
|
788 |
opens a theory target (cf.\ \secref{sec:target}) which allows to
|
|
789 |
specify constants with overloaded definitions. These are identified
|
|
790 |
by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type
|
|
791 |
instances. The definitions themselves are established using common
|
|
792 |
specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as
|
|
793 |
reference to the corresponding constants. The target is concluded
|
|
794 |
by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
|
|
795 |
|
|
796 |
A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
|
|
797 |
the corresponding definition, which is occasionally useful for
|
|
798 |
exotic overloading. It is at the discretion of the user to avoid
|
|
799 |
malformed theory specifications!
|
|
800 |
|
|
801 |
\end{descr}%
|
|
802 |
\end{isamarkuptext}%
|
|
803 |
\isamarkuptrue%
|
|
804 |
%
|
|
805 |
\isamarkupsection{Incorporating ML code \label{sec:ML}%
|
|
806 |
}
|
|
807 |
\isamarkuptrue%
|
|
808 |
%
|
|
809 |
\begin{isamarkuptext}%
|
|
810 |
\begin{matharray}{rcl}
|
|
811 |
\indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
|
|
812 |
\indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
|
|
813 |
\indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
|
|
814 |
\indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
|
|
815 |
\indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
|
|
816 |
\indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\
|
|
817 |
\end{matharray}
|
|
818 |
|
|
819 |
\begin{rail}
|
|
820 |
'use' name
|
|
821 |
;
|
|
822 |
('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
|
|
823 |
;
|
|
824 |
'method\_setup' name '=' text text
|
|
825 |
;
|
|
826 |
\end{rail}
|
|
827 |
|
|
828 |
\begin{descr}
|
|
829 |
|
|
830 |
\item [\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML
|
|
831 |
commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
|
|
832 |
down to the ML toplevel and may be modified, using \verb|"Context.>>"| or derived ML commands. The file name is checked with
|
|
833 |
the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
|
|
834 |
header (see also \secref{sec:begin-thy}).
|
|
835 |
|
|
836 |
\item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
|
|
837 |
|
|
838 |
\item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
|
|
839 |
diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context
|
|
840 |
may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
|
|
841 |
at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
|
|
842 |
|
|
843 |
\item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
|
|
844 |
context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
|
|
845 |
of type \verb|"theory -> theory"|. This enables to initialize
|
|
846 |
any object-logic specific tools and packages written in ML, for
|
|
847 |
example.
|
|
848 |
|
|
849 |
\item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
|
|
850 |
defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%
|
|
851 |
\verb| Proof.context -> Proof.method"|. Parsing concrete method syntax
|
|
852 |
from \verb|Args.src| input can be quite tedious in general. The
|
|
853 |
following simple examples are for methods without any explicit
|
|
854 |
arguments, or a list of theorems, respectively.
|
|
855 |
|
|
856 |
%FIXME proper antiquotations
|
|
857 |
{\footnotesize
|
|
858 |
\begin{verbatim}
|
|
859 |
Method.no_args (Method.METHOD (fn facts => foobar_tac))
|
|
860 |
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
|
|
861 |
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
|
|
862 |
Method.thms_ctxt_args (fn thms => fn ctxt =>
|
|
863 |
Method.METHOD (fn facts => foobar_tac))
|
|
864 |
\end{verbatim}
|
|
865 |
}
|
|
866 |
|
|
867 |
Note that mere tactic emulations may ignore the \isa{facts}
|
|
868 |
parameter above. Proper proof methods would do something
|
|
869 |
appropriate with the list of current facts, though. Single-rule
|
|
870 |
methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
|
|
871 |
using \verb|Method.insert_tac| before applying the main tactic.
|
|
872 |
|
|
873 |
\end{descr}%
|
|
874 |
\end{isamarkuptext}%
|
|
875 |
\isamarkuptrue%
|
|
876 |
%
|
|
877 |
\isamarkupsection{Primitive specification elements%
|
|
878 |
}
|
|
879 |
\isamarkuptrue%
|
|
880 |
%
|
|
881 |
\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
|
|
882 |
}
|
|
883 |
\isamarkuptrue%
|
|
884 |
%
|
|
885 |
\begin{isamarkuptext}%
|
|
886 |
\begin{matharray}{rcll}
|
|
887 |
\indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
|
|
888 |
\indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
|
|
889 |
\indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
|
|
890 |
\indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
|
|
891 |
\end{matharray}
|
|
892 |
|
|
893 |
\begin{rail}
|
|
894 |
'classes' (classdecl +)
|
|
895 |
;
|
|
896 |
'classrel' (nameref ('<' | subseteq) nameref + 'and')
|
|
897 |
;
|
|
898 |
'defaultsort' sort
|
|
899 |
;
|
|
900 |
\end{rail}
|
|
901 |
|
|
902 |
\begin{descr}
|
|
903 |
|
|
904 |
\item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]
|
|
905 |
declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. Cyclic class structures are not permitted.
|
|
906 |
|
|
907 |
\item [\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states
|
|
908 |
subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and
|
|
909 |
\isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \secref{sec:axclass}) provides a way to
|
|
910 |
introduce proven class relations.
|
|
911 |
|
|
912 |
\item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the
|
|
913 |
new default sort for any type variables given without sort
|
|
914 |
constraints. Usually, the default sort would be only changed when
|
|
915 |
defining a new object-logic.
|
|
916 |
|
|
917 |
\item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
|
|
918 |
using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
|
|
919 |
|
|
920 |
\end{descr}%
|
|
921 |
\end{isamarkuptext}%
|
|
922 |
\isamarkuptrue%
|
|
923 |
%
|
|
924 |
\isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
|
|
925 |
}
|
|
926 |
\isamarkuptrue%
|
|
927 |
%
|
|
928 |
\begin{isamarkuptext}%
|
|
929 |
\begin{matharray}{rcll}
|
|
930 |
\indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\
|
|
931 |
\indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\
|
|
932 |
\indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\
|
|
933 |
\indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
|
|
934 |
\end{matharray}
|
|
935 |
|
|
936 |
\begin{rail}
|
|
937 |
'types' (typespec '=' type infix? +)
|
|
938 |
;
|
|
939 |
'typedecl' typespec infix?
|
|
940 |
;
|
|
941 |
'nonterminals' (name +)
|
|
942 |
;
|
|
943 |
'arities' (nameref '::' arity +)
|
|
944 |
;
|
|
945 |
\end{rail}
|
|
946 |
|
|
947 |
\begin{descr}
|
|
948 |
|
|
949 |
\item [\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}}]
|
|
950 |
introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}
|
|
951 |
for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as
|
|
952 |
are available in Isabelle/HOL for example, type synonyms are just
|
|
953 |
purely syntactic abbreviations without any logical significance.
|
|
954 |
Internally, type synonyms are fully expanded.
|
|
955 |
|
|
956 |
\item [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]
|
|
957 |
declares a new type constructor \isa{t}, intended as an actual
|
|
958 |
logical type (of the object-logic, if available).
|
|
959 |
|
|
960 |
\item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type
|
|
961 |
constructors \isa{c} (without arguments) to act as purely
|
|
962 |
syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
|
|
963 |
syntax of terms or types.
|
|
964 |
|
|
965 |
\item [\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type
|
|
966 |
constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \S\ref{sec:axclass}) provides a way to
|
|
967 |
introduce proven type arities.
|
|
968 |
|
|
969 |
\end{descr}%
|
|
970 |
\end{isamarkuptext}%
|
|
971 |
\isamarkuptrue%
|
|
972 |
%
|
|
973 |
\isamarkupsubsection{Constants and definitions \label{sec:consts}%
|
|
974 |
}
|
|
975 |
\isamarkuptrue%
|
|
976 |
%
|
|
977 |
\begin{isamarkuptext}%
|
|
978 |
Definitions essentially express abbreviations within the logic. The
|
|
979 |
simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
|
|
980 |
where the arguments of \isa{c} appear on the left, abbreviating a
|
|
981 |
prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
|
|
982 |
written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
|
|
983 |
definitions may be weakened by adding arbitrary pre-conditions:
|
|
984 |
\isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
|
|
985 |
|
|
986 |
\medskip The built-in well-formedness conditions for definitional
|
|
987 |
specifications are:
|
|
988 |
|
|
989 |
\begin{itemize}
|
|
990 |
|
|
991 |
\item Arguments (on the left-hand side) must be distinct variables.
|
|
992 |
|
|
993 |
\item All variables on the right-hand side must also appear on the
|
|
994 |
left-hand side.
|
|
995 |
|
|
996 |
\item All type variables on the right-hand side must also appear on
|
|
997 |
the left-hand side; this prohibits \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} for example.
|
|
998 |
|
|
999 |
\item The definition must not be recursive. Most object-logics
|
|
1000 |
provide definitional principles that can be used to express
|
|
1001 |
recursion safely.
|
|
1002 |
|
|
1003 |
\end{itemize}
|
|
1004 |
|
|
1005 |
Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
|
|
1006 |
recursively at type instances corresponding to the immediate
|
|
1007 |
argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
|
|
1008 |
specification patterns impose global constraints on all occurrences,
|
|
1009 |
e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
|
|
1010 |
corresponding occurrences on some right-hand side need to be an
|
|
1011 |
instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
|
|
1012 |
|
|
1013 |
\begin{matharray}{rcl}
|
|
1014 |
\indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
|
|
1015 |
\indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\
|
|
1016 |
\indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isartrans{theory}{theory} \\
|
|
1017 |
\end{matharray}
|
|
1018 |
|
|
1019 |
\begin{rail}
|
|
1020 |
'consts' ((name '::' type mixfix?) +)
|
|
1021 |
;
|
|
1022 |
'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
|
|
1023 |
;
|
|
1024 |
\end{rail}
|
|
1025 |
|
|
1026 |
\begin{rail}
|
|
1027 |
'constdefs' structs? (constdecl? constdef +)
|
|
1028 |
;
|
|
1029 |
|
|
1030 |
structs: '(' 'structure' (vars + 'and') ')'
|
|
1031 |
;
|
|
1032 |
constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
|
|
1033 |
;
|
|
1034 |
constdef: thmdecl? prop
|
|
1035 |
;
|
|
1036 |
\end{rail}
|
|
1037 |
|
|
1038 |
\begin{descr}
|
|
1039 |
|
|
1040 |
\item [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant
|
|
1041 |
\isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
|
|
1042 |
optional mixfix annotations may attach concrete syntax to the
|
|
1043 |
constants declared.
|
|
1044 |
|
|
1045 |
\item [\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn}
|
|
1046 |
as a definitional axiom for some existing constant.
|
|
1047 |
|
|
1048 |
The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
|
|
1049 |
for this definition, which is occasionally useful for exotic
|
|
1050 |
overloading. It is at the discretion of the user to avoid malformed
|
|
1051 |
theory specifications!
|
|
1052 |
|
|
1053 |
The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
|
|
1054 |
potentially overloaded. Unless this option is given, a warning
|
|
1055 |
message would be issued for any definitional equation with a more
|
|
1056 |
special type than that of the corresponding constant declaration.
|
|
1057 |
|
|
1058 |
\item [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}] provides a streamlined combination of
|
|
1059 |
constants declarations and definitions: type-inference takes care of
|
|
1060 |
the most general typing of the given specification (the optional
|
|
1061 |
type constraint may refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The resulting type declaration needs to agree with
|
|
1062 |
that of the specification; overloading is \emph{not} supported here!
|
|
1063 |
|
|
1064 |
The constant name may be omitted altogether, if neither type nor
|
|
1065 |
syntax declarations are given. The canonical name of the
|
|
1066 |
definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
|
|
1067 |
unless specified otherwise. Also note that the given list of
|
|
1068 |
specifications is processed in a strictly sequential manner, with
|
|
1069 |
type-checking being performed independently.
|
|
1070 |
|
|
1071 |
An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
|
|
1072 |
admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
|
|
1073 |
particularly useful with locales (see also \S\ref{sec:locale}).
|
|
1074 |
|
|
1075 |
\end{descr}%
|
|
1076 |
\end{isamarkuptext}%
|
|
1077 |
\isamarkuptrue%
|
|
1078 |
%
|
|
1079 |
\isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
|
|
1080 |
}
|
|
1081 |
\isamarkuptrue%
|
|
1082 |
%
|
|
1083 |
\begin{isamarkuptext}%
|
|
1084 |
\begin{matharray}{rcll}
|
|
1085 |
\indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
|
|
1086 |
\indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
27047
|
1087 |
\indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isarkeep{local{\dsh}theory} \\
|
27042
|
1088 |
\end{matharray}
|
|
1089 |
|
|
1090 |
\begin{rail}
|
|
1091 |
'axioms' (axmdecl prop +)
|
|
1092 |
;
|
|
1093 |
('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
|
|
1094 |
;
|
|
1095 |
\end{rail}
|
|
1096 |
|
|
1097 |
\begin{descr}
|
|
1098 |
|
|
1099 |
\item [\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduces arbitrary
|
|
1100 |
statements as axioms of the meta-logic. In fact, axioms are
|
|
1101 |
``axiomatic theorems'', and may be referred later just as any other
|
|
1102 |
theorem.
|
|
1103 |
|
|
1104 |
Axioms are usually only introduced when declaring new logical
|
|
1105 |
systems. Everyday work is typically done the hard way, with proper
|
|
1106 |
definitions and proven theorems.
|
|
1107 |
|
|
1108 |
\item [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
|
|
1109 |
retrieves and stores existing facts in the theory context, or the
|
|
1110 |
specified target context (see also \secref{sec:target}). Typical
|
|
1111 |
applications would also involve attributes, to declare Simplifier
|
|
1112 |
rules, for example.
|
|
1113 |
|
|
1114 |
\item [\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}] is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts.
|
|
1115 |
|
|
1116 |
\end{descr}%
|
|
1117 |
\end{isamarkuptext}%
|
|
1118 |
\isamarkuptrue%
|
|
1119 |
%
|
|
1120 |
\isamarkupsection{Oracles%
|
|
1121 |
}
|
|
1122 |
\isamarkuptrue%
|
|
1123 |
%
|
|
1124 |
\begin{isamarkuptext}%
|
|
1125 |
\begin{matharray}{rcl}
|
|
1126 |
\indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
|
|
1127 |
\end{matharray}
|
|
1128 |
|
|
1129 |
The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
|
|
1130 |
type \verb|T| given by the user. This acts like an infinitary
|
|
1131 |
specification of axioms -- there is no internal check of the
|
|
1132 |
correctness of the results! The inference kernel records oracle
|
|
1133 |
invocations within the internal derivation object of theorems, and
|
|
1134 |
the pretty printer attaches ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results
|
|
1135 |
that are not fully checked by Isabelle inferences.
|
|
1136 |
|
|
1137 |
\begin{rail}
|
|
1138 |
'oracle' name '(' type ')' '=' text
|
|
1139 |
;
|
|
1140 |
\end{rail}
|
|
1141 |
|
|
1142 |
\begin{descr}
|
|
1143 |
|
|
1144 |
\item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
|
|
1145 |
given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
|
|
1146 |
\verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
|
|
1147 |
ML function of type
|
|
1148 |
\verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
|
|
1149 |
bound to the global identifier \verb|name|.
|
|
1150 |
|
|
1151 |
\end{descr}%
|
|
1152 |
\end{isamarkuptext}%
|
|
1153 |
\isamarkuptrue%
|
|
1154 |
%
|
|
1155 |
\isamarkupsection{Name spaces%
|
|
1156 |
}
|
|
1157 |
\isamarkuptrue%
|
|
1158 |
%
|
|
1159 |
\begin{isamarkuptext}%
|
|
1160 |
\begin{matharray}{rcl}
|
|
1161 |
\indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\
|
|
1162 |
\indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\
|
|
1163 |
\indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isartrans{theory}{theory} \\
|
|
1164 |
\end{matharray}
|
|
1165 |
|
|
1166 |
\begin{rail}
|
|
1167 |
'hide' ('(open)')? name (nameref + )
|
|
1168 |
;
|
|
1169 |
\end{rail}
|
|
1170 |
|
|
1171 |
Isabelle organizes any kind of name declarations (of types,
|
|
1172 |
constants, theorems etc.) by separate hierarchically structured name
|
|
1173 |
spaces. Normally the user does not have to control the behavior of
|
|
1174 |
name spaces by hand, yet the following commands provide some way to
|
|
1175 |
do so.
|
|
1176 |
|
|
1177 |
\begin{descr}
|
|
1178 |
|
|
1179 |
\item [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the
|
|
1180 |
current name declaration mode. Initially, theories start in
|
|
1181 |
\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically
|
|
1182 |
qualified by the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}
|
|
1183 |
causes all names to be declared without the theory prefix, until
|
|
1184 |
\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
|
|
1185 |
|
|
1186 |
Note that global names are prone to get hidden accidently later,
|
|
1187 |
when qualified names of the same base name are introduced.
|
|
1188 |
|
|
1189 |
\item [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes
|
|
1190 |
declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
|
|
1191 |
\isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global
|
|
1192 |
(unqualified) names may never be hidden.
|
|
1193 |
|
|
1194 |
Note that hiding name space accesses has no impact on logical
|
|
1195 |
declarations -- they remain valid internally. Entities that are no
|
|
1196 |
longer accessible to the user are printed with the special qualifier
|
|
1197 |
``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
|
|
1198 |
|
|
1199 |
\end{descr}%
|
|
1200 |
\end{isamarkuptext}%
|
|
1201 |
\isamarkuptrue%
|
|
1202 |
%
|
|
1203 |
\isamarkupsection{Syntax and translations \label{sec:syn-trans}%
|
|
1204 |
}
|
|
1205 |
\isamarkuptrue%
|
|
1206 |
%
|
|
1207 |
\begin{isamarkuptext}%
|
|
1208 |
\begin{matharray}{rcl}
|
|
1209 |
\indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\
|
|
1210 |
\indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
|
|
1211 |
\indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\
|
|
1212 |
\indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\
|
|
1213 |
\end{matharray}
|
|
1214 |
|
|
1215 |
\begin{rail}
|
|
1216 |
('syntax' | 'no\_syntax') mode? (constdecl +)
|
|
1217 |
;
|
|
1218 |
('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
|
|
1219 |
;
|
|
1220 |
|
|
1221 |
mode: ('(' ( name | 'output' | name 'output' ) ')')
|
|
1222 |
;
|
|
1223 |
transpat: ('(' nameref ')')? string
|
|
1224 |
;
|
|
1225 |
\end{rail}
|
|
1226 |
|
|
1227 |
\begin{descr}
|
|
1228 |
|
|
1229 |
\item [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to
|
|
1230 |
\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical
|
|
1231 |
signature extension is omitted. Thus the context free grammar of
|
|
1232 |
Isabelle's inner syntax may be augmented in arbitrary ways,
|
|
1233 |
independently of the logic. The \isa{mode} argument refers to the
|
|
1234 |
print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
|
|
1235 |
input and output grammar.
|
|
1236 |
|
|
1237 |
\item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
|
|
1238 |
grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
|
|
1239 |
|
|
1240 |
\item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic
|
|
1241 |
translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
|
|
1242 |
parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
|
|
1243 |
Translation patterns may be prefixed by the syntactic category to be
|
|
1244 |
used for parsing; the default is \isa{logic}.
|
|
1245 |
|
|
1246 |
\item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
|
|
1247 |
translation rules, which are interpreted in the same manner as for
|
|
1248 |
\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
|
|
1249 |
|
|
1250 |
\end{descr}%
|
|
1251 |
\end{isamarkuptext}%
|
|
1252 |
\isamarkuptrue%
|
|
1253 |
%
|
|
1254 |
\isamarkupsection{Syntax translation functions%
|
|
1255 |
}
|
|
1256 |
\isamarkuptrue%
|
|
1257 |
%
|
|
1258 |
\begin{isamarkuptext}%
|
|
1259 |
\begin{matharray}{rcl}
|
|
1260 |
\indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
|
|
1261 |
\indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
|
|
1262 |
\indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
|
|
1263 |
\indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
|
|
1264 |
\indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
|
|
1265 |
\indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
|
|
1266 |
\end{matharray}
|
|
1267 |
|
|
1268 |
\begin{rail}
|
|
1269 |
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
|
|
1270 |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
|
|
1271 |
;
|
|
1272 |
|
|
1273 |
'token\_translation' text
|
|
1274 |
;
|
|
1275 |
\end{rail}
|
|
1276 |
|
|
1277 |
Syntax translation functions written in ML admit almost arbitrary
|
|
1278 |
manipulations of Isabelle's inner syntax. Any of the above commands
|
|
1279 |
have a single \railqtok{text} argument that refers to an ML
|
|
1280 |
expression of appropriate type, which are as follows by default:
|
|
1281 |
|
|
1282 |
%FIXME proper antiquotations
|
|
1283 |
\begin{ttbox}
|
|
1284 |
val parse_ast_translation : (string * (ast list -> ast)) list
|
|
1285 |
val parse_translation : (string * (term list -> term)) list
|
|
1286 |
val print_translation : (string * (term list -> term)) list
|
|
1287 |
val typed_print_translation :
|
|
1288 |
(string * (bool -> typ -> term list -> term)) list
|
|
1289 |
val print_ast_translation : (string * (ast list -> ast)) list
|
|
1290 |
val token_translation :
|
|
1291 |
(string * string * (string -> string * real)) list
|
|
1292 |
\end{ttbox}
|
|
1293 |
|
|
1294 |
If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
|
|
1295 |
translation functions may depend on the current theory or proof
|
|
1296 |
context. This allows to implement advanced syntax mechanisms, as
|
|
1297 |
translations functions may refer to specific theory declarations or
|
|
1298 |
auxiliary proof data.
|
|
1299 |
|
|
1300 |
See also \cite[\S8]{isabelle-ref} for more information on the
|
|
1301 |
general concept of syntax transformations in Isabelle.
|
|
1302 |
|
|
1303 |
%FIXME proper antiquotations
|
|
1304 |
\begin{ttbox}
|
|
1305 |
val parse_ast_translation:
|
27047
|
1306 |
(string * (Proof.context -> ast list -> ast)) list
|
27042
|
1307 |
val parse_translation:
|
27047
|
1308 |
(string * (Proof.context -> term list -> term)) list
|
27042
|
1309 |
val print_translation:
|
27047
|
1310 |
(string * (Proof.context -> term list -> term)) list
|
27042
|
1311 |
val typed_print_translation:
|
27047
|
1312 |
(string * (Proof.context -> bool -> typ -> term list -> term)) list
|
27042
|
1313 |
val print_ast_translation:
|
27047
|
1314 |
(string * (Proof.context -> ast list -> ast)) list
|
27042
|
1315 |
\end{ttbox}%
|
|
1316 |
\end{isamarkuptext}%
|
|
1317 |
\isamarkuptrue%
|
|
1318 |
%
|
26869
|
1319 |
\isadelimtheory
|
|
1320 |
%
|
|
1321 |
\endisadelimtheory
|
|
1322 |
%
|
|
1323 |
\isatagtheory
|
|
1324 |
\isacommand{end}\isamarkupfalse%
|
|
1325 |
%
|
|
1326 |
\endisatagtheory
|
|
1327 |
{\isafoldtheory}%
|
|
1328 |
%
|
|
1329 |
\isadelimtheory
|
|
1330 |
%
|
|
1331 |
\endisadelimtheory
|
|
1332 |
\isanewline
|
|
1333 |
\end{isabellebody}%
|
|
1334 |
%%% Local Variables:
|
|
1335 |
%%% mode: latex
|
|
1336 |
%%% TeX-master: "root"
|
|
1337 |
%%% End:
|