3 \def\isabellecontext{Spec}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Main\isanewline
21 \isamarkupchapter{Theory specifications%
25 \begin{isamarkuptext}%
26 The Isabelle/Isar theory format integrates specifications and
27 proofs, supporting interactive development with unlimited undo
28 operation. There is an integrated document preparation system (see
29 \chref{ch:document-prep}), for typesetting formal developments
30 together with informal text. The resulting hyper-linked PDF
31 documents can be used both for WWW presentation and printed copies.
33 The Isar proof language (see \chref{ch:proofs}) is embedded into the
34 theory language as a proper sub-language. Proof mode is entered by
35 stating some \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory
36 level, and left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}). Some theory specification mechanisms also require a proof,
37 such as \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} in HOL, which demands non-emptiness of
38 the representing sets.%
42 \isamarkupsection{Defining theories \label{sec:begin-thy}%
46 \begin{isamarkuptext}%
47 \begin{matharray}{rcl}
48 \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isa{{\isachardoublequote}toplevel\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
49 \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ toplevel{\isachardoublequote}} \\
52 Isabelle/Isar theories are defined via theory files, which may
53 contain both specifications and proofs; occasionally definitional
54 mechanisms also require some explicit proof. The theory body may be
55 sub-structured by means of \emph{local theory targets}, such as
56 \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}.
58 The first proper command of a theory is \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which
59 indicates imports of previous theories and optional dependencies on
60 other source files (usually in ML). Just preceding the initial
61 \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} command there may be an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is only relevant to document
62 preparation: see also the other section markup commands in
65 A theory is concluded by a final \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command,
66 one that does not belong to a local theory target. No further
67 commands may follow such a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}},
68 although some user-interfaces might pretend that trailing input is
72 'theory' name 'imports' (name +) uses? 'begin'
75 uses: 'uses' ((name | parname) +);
80 \item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}
81 starts a new theory \isa{A} based on the merge of existing
82 theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
84 Due to the possibility to import more than one ancestor, the
85 resulting theory structure of an Isabelle session forms a directed
86 acyclic graph (DAG). Isabelle's theory loader ensures that the
87 sources contributing to the development graph are always up-to-date:
88 changed files are automatically reloaded whenever a theory header
89 specification is processed.
91 The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional
92 dependencies on extra files (usually ML sources). Files will be
93 loaded immediately (as ML), unless the name is parenthesized. The
94 latter case records a dependency that needs to be resolved later in
95 the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files;
96 other file formats require specific load commands defined by the
97 corresponding tools or packages.
99 \item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory
100 definition. Note that local theory targets involve a local
101 \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting.
107 \isamarkupsection{Local theory targets \label{sec:target}%
111 \begin{isamarkuptext}%
112 A local theory target is a context managed separately within the
113 enclosing theory. Contexts may introduce parameters (fixed
114 variables) and assumptions (hypotheses). Definitions and theorems
115 depending on the context may be added incrementally later on. Named
116 contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
117 (cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
118 global theory context.
120 \begin{matharray}{rcll}
121 \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
122 \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
125 \indexouternonterm{target}
127 'context' name 'begin'
130 target: '(' 'in' name ')'
136 \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}} recommences an
137 existing locale or class context \isa{c}. Note that locale and
138 class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as
139 well, in order to continue the local theory immediately after the
140 initial specification.
142 \item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory
143 and continues the enclosing global theory. Note that a global
144 \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
145 theory itself (\secref{sec:begin-thy}).
147 \item \isa{{\isachardoublequote}{\isacharparenleft}{\isachardoublequote}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isachardoublequote}c{\isacharparenright}{\isachardoublequote}} given after any
148 local theory command specifies an immediate target, e.g.\
149 ``\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
150 global theory context; the current target context will be suspended
151 for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
152 always produce a global result independently of the current target
157 The exact meaning of results produced within a local theory context
158 depends on the underlying target infrastructure (locale, type class
159 etc.). The general idea is as follows, considering a context named
160 \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
162 Definitions are exported by introducing a global version with
163 additional arguments; a syntactic abbreviation links the long form
164 with the abstract version of the target context. For example,
165 \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
166 level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
167 abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
168 fixed parameter \isa{x}).
170 Theorems are exported by discharging the assumptions and
171 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
172 \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
176 \isamarkupsection{Basic specification elements%
180 \begin{isamarkuptext}%
181 \begin{matharray}{rcll}
182 \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!)\\
183 \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
184 \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\
185 \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
186 \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}\ {\isachardoublequote}} \\
189 These specification mechanisms provide a slightly more abstract view
190 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
191 \secref{sec:axms-thms}). In particular, type-inference is commonly
192 available, and result names need not be given.
195 'axiomatization' target? fixes? ('where' specs)?
197 'definition' target? (decl 'where')? thmdecl? prop
199 'abbreviation' target? mode? (decl 'where')? prop
202 fixes: ((name ('::' type)? mixfix? | vars) + 'and')
204 specs: (thmdecl? props + 'and')
206 decl: name ('::' type)? mixfix?
212 \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}}
213 introduces several constants simultaneously and states axiomatic
214 properties for these. The constants are marked as being specified
215 once and for all, which prevents additional specifications being
218 Note that axiomatic specifications are only appropriate when
219 declaring a new logical system; axiomatic specifications are
220 restricted to global theory contexts. Normal applications should
221 only use definitional mechanisms!
223 \item \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}} produces an
224 internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
225 given as \isa{eq}, which is then turned into a proven fact. The
226 given proposition may deviate from internal meta-level equality
227 according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
228 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
229 change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
231 Definitions may be presented with explicit arguments on the LHS, as
232 well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
233 \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
234 unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
236 \item \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}} introduces a
237 syntactic constant which is associated with a certain term according
238 to the meta-level equality \isa{eq}.
240 Abbreviations participate in the usual type-inference process, but
241 are expanded before the logic ever sees them. Pretty printing of
242 terms involves higher-order rewriting with rules stemming from
243 reverted abbreviations. This needs some care to avoid overlapping
244 or looping syntactic replacements!
246 The optional \isa{mode} specification restricts output to a
247 particular print mode; using ``\isa{input}'' here achieves the
248 effect of one-way abbreviations. The mode may also include an
249 ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
250 declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
251 \secref{sec:syn-trans}.
253 \item \hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}} prints all constant abbreviations
254 of the current context.
260 \isamarkupsection{Generic declarations%
264 \begin{isamarkuptext}%
265 Arbitrary operations on the background context may be wrapped-up as
266 generic declaration elements. Since the underlying concept of local
267 theories may be subject to later re-interpretation, there is an
268 additional dependency on a morphism that tells the difference of the
269 original declaration context wrt.\ the application context
270 encountered later on. A fact declaration is an important special
271 case: it consists of a theorem which is applied to the context by
272 means of an attribute.
274 \begin{matharray}{rcl}
275 \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
276 \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
280 'declaration' target? text
282 'declare' target? (thmrefs + 'and')
288 \item \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d} adds the declaration
289 function \isa{d} of ML type \verb|declaration|, to the current
290 local theory under construction. In later application contexts, the
291 function is transformed according to the morphisms being involved in
292 the interpretation hierarchy.
294 \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
295 current local theory context. No theorem binding is involved here,
296 unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
297 \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
298 of applying attributes as included in the theorem specification.
304 \isamarkupsection{Locales \label{sec:locale}%
308 \begin{isamarkuptext}%
309 Locales are named local contexts, consisting of a list of
310 declaration elements that are modeled after the Isar proof context
311 commands (cf.\ \secref{sec:proof-context}).%
315 \isamarkupsubsection{Locale specifications%
319 \begin{isamarkuptext}%
320 \begin{matharray}{rcl}
321 \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
322 \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
323 \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
324 \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isa{method} \\
325 \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\
328 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
329 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
330 \indexisarelem{defines}\indexisarelem{notes}
332 'locale' name ('=' localeexpr)? 'begin'?
334 'print\_locale' '!'? localeexpr
336 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
339 contextexpr: nameref | '(' contextexpr ')' |
340 (contextexpr (name mixfix? +)) | (contextexpr + '+')
342 contextelem: fixes | constrains | assumes | defines | notes
344 fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
346 constrains: 'constrains' (name '::' type + 'and')
348 assumes: 'assumes' (thmdecl? props + 'and')
350 defines: 'defines' (thmdecl? prop proppat? + 'and')
352 notes: 'notes' (thmdef? thmrefs + 'and')
358 \item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}} defines a
359 new locale \isa{loc} as a context consisting of a certain view of
360 existing locales (\isa{import}) plus some additional elements
361 (\isa{body}). Both \isa{import} and \isa{body} are optional;
362 the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
363 locale, which may still be useful to collect declarations of facts
364 later on. Type-inference on locale expressions automatically takes
365 care of the most general typing that the combined context elements
368 The \isa{import} consists of a structured context expression,
369 consisting of references to existing locales, renamed contexts, or
370 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
371 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
372 position. Renaming by default deletes concrete syntax, but new
373 syntax may by specified with a mixfix annotation. An exeption of
374 this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
375 be changed. Merging proceeds from left-to-right, suppressing any
376 duplicates stemming from different paths through the import
379 The \isa{body} consists of basic context elements, further context
380 expressions may be included as well.
384 \item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares a local
385 parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
386 are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
387 implicitly in this context.
389 \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type
390 constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
392 \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}
393 introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
394 proof (cf.\ \secref{sec:proof-context}).
396 \item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} defines a previously
397 declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
398 proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
399 takes an equational proposition instead of variable-term pair. The
400 left-hand side of the equation may have additional arguments, e.g.\
401 ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
403 \item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}
404 reconsiders facts within a local context. Most notably, this may
405 include arbitrary declarations in any attribute specifications
406 included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
408 The initial \isa{import} specification of a locale expression
409 maintains a dynamic relation to the locales being referenced
410 (benefiting from any later fact declarations in the obvious manner).
414 Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
415 in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
416 are illegal in locale definitions. In the long goal format of
417 \secref{sec:goals}, term bindings may be included as expected,
420 \medskip By default, locale specifications are ``closed up'' by
421 turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
422 (modulo local definitions). The predicate statement covers only the
423 newly specified assumptions, omitting the content of included locale
424 expressions. The full cumulative view is only provided on export,
425 involving another predicate \isa{loc} that refers to the complete
428 In any case, the predicate arguments are those locale parameters
429 that actually occur in the respective piece of text. Also note that
430 these predicates operate at the meta-level in theory, but the locale
431 packages attempts to internalize statements according to the
432 object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
433 \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
434 \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
436 \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
437 specified locale expression in a flattened form. The notable
438 special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
439 contents of the named locale, but keep in mind that type-inference
440 will normalize type variables according to the usual alphabetical
441 order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
442 Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
444 \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
445 of the current theory.
447 \item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}
448 repeatedly expand all introduction rules of locale predicates of the
449 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
450 assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
451 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
452 specifications entailed by the context, both from target statements,
453 and from interpretations (see below). New goals that are entailed
454 by the current context are discharged automatically.
460 \isamarkupsubsection{Interpretation of locales%
464 \begin{isamarkuptext}%
465 Locale expressions (more precisely, \emph{context expressions}) may
466 be instantiated, and the instantiated facts added to the current
467 context. This requires a proof of the instantiated specification
468 and is called \emph{locale interpretation}. Interpretation is
469 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}}}}).
471 \begin{matharray}{rcl}
472 \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
473 \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
476 \indexouternonterm{interp}
478 'interpretation' (interp | name ('<' | subseteq) contextexpr)
482 instantiation: ('[' (inst+) ']')?
484 interp: (name ':')? \\ (contextexpr instantiation |
485 name instantiation 'where' (thmdecl? prop + 'and'))
491 \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
493 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
494 \isa{insts} and is positional. All parameters must receive an
495 instantiation term --- with the exception of defined parameters.
496 These are, if omitted, derived from the defining equation and other
497 instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
499 The command generates proof obligations for the instantiated
500 specifications (assumes and defines elements). Once these are
501 discharged by the user, instantiated facts are added to the theory
502 in a post-processing phase.
504 Additional equations, which are unfolded in facts during
505 post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
506 This is useful for interpreting concepts introduced through
507 definition specification elements. The equations must be proved.
508 Note that if equations are present, the context expression is
509 restricted to a locale name.
511 The command is aware of interpretations already active in the
512 theory, but does not simplify the goal automatically. In order to
513 simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}
514 or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}. Post-processing is not applied to
515 facts of interpretations that are already active. This avoids
516 duplication of interpreted facts, in particular. Note that, in the
517 case of a locale with import, parts of the interpretation may
518 already be active. The command will only process facts for new
521 The context expression may be preceded by a name, which takes effect
522 in the post-processing of facts. It is used to prefix fact names,
523 for example to avoid accidental hiding of other facts.
525 Adding facts to locales has the effect of adding interpreted facts
526 to the theory for all active interpretations also. That is,
527 interpretations dynamically participate in any facts added to
530 \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
532 This form of the command interprets \isa{expr} in the locale
533 \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the
534 localized version of the theorem command, the proof is in the
535 context of \isa{name}. After the proof obligation has been
536 dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
537 context \isa{name} is subsequently entered. Note that, like
538 import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
539 Like facts of renamed context elements, facts obtained by
540 interpretation may be accessed by prefixing with the parameter
541 renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
543 Unlike interpretation in theories, instantiation is confined to the
544 renaming of parameters, which may be specified as part of the
545 context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
547 Only specification fragments of \isa{expr} that are not already
548 part of \isa{name} (be it imported, derived or a derived fragment
549 of the import) are considered by interpretation. This enables
550 circular interpretations.
552 If interpretations of \isa{name} exist in the current theory, the
553 command adds interpretations for \isa{expr} as well, with the same
554 prefix and attributes, although only for fragments of \isa{expr}
555 that are not interpreted in the theory already.
557 \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
558 interprets \isa{expr} in the proof context and is otherwise
559 similar to interpretation in theories.
564 Since attributes are applied to interpreted theorems,
565 interpretation may modify the context of common proof tools, e.g.\
566 the Simplifier or Classical Reasoner. Since the behavior of such
567 automated reasoning tools is \emph{not} stable under
568 interpretation morphisms, manual declarations might have to be
573 An interpretation in a theory may subsume previous
574 interpretations. This happens if the same specification fragment
575 is interpreted twice and the instantiation of the second
576 interpretation is more general than the interpretation of the
577 first. A warning is issued, since it is likely that these could
578 have been generalized in the first place. The locale package does
579 not attempt to remove subsumed interpretations.
584 \isamarkupsection{Classes \label{sec:class}%
588 \begin{isamarkuptext}%
589 A class is a particular locale with \emph{exactly one} type variable
590 \isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
591 is established which is interpreted logically as axiomatic type
592 class \cite{Wenzel:1997:TPHOL} whose logical content are the
593 assumptions of the locale. Thus, classes provide the full
594 generality of locales combined with the commodity of type classes
595 (notably type-inference). See \cite{isabelle-classes} for a short
598 \begin{matharray}{rcl}
599 \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
600 \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
601 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
602 \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
603 \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
604 \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
605 \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\
609 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
612 'instantiation' (nameref + 'and') '::' arity 'begin'
616 'subclass' target? nameref
623 superclassexpr: nameref | (nameref '+' superclassexpr)
629 \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}} defines
630 a new class \isa{c}, inheriting from \isa{superclasses}. This
631 introduces a locale \isa{c} with import of all locales \isa{superclasses}.
633 Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
634 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
635 \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
637 Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
638 mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
639 corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
640 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
641 --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
642 class membership proofs.
644 \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.\ \secref{sec:target}) which
645 allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding
646 to sort \isa{s} at the 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 in the
647 target body poses a goal stating these type arities. The target is
648 concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
650 Note that a list of simultaneous type constructors may be given;
651 this corresponds nicely to mutual recursive type definitions, e.g.\
654 \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
655 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
656 the type classes involved. After finishing the proof, the
657 background theory will be augmented by the proven type arities.
659 \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
660 \isa{d} sets up a goal stating that class \isa{c} is logically
661 contained in class \isa{d}. After finishing the proof, class
662 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
664 \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
667 \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes all classes and their
668 subclass relations as a Hasse diagram.
670 \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class
671 introduction rules of this theory. Note that this method usually
672 needs not be named explicitly, as it is already included in the
673 default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
674 instantiation of trivial (syntactic) classes may be performed by a
675 single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
681 \isamarkupsubsection{The class target%
685 \begin{isamarkuptext}%
688 A named context may refer to a locale (cf.\ \secref{sec:target}).
689 If this locale is also a class \isa{c}, apart from the common
690 locale target behaviour the following happens.
694 \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
695 local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
696 are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
697 referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
699 \item Local theorem bindings are lifted as are assumptions.
701 \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
702 global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
703 resolves ambiguities. In rare cases, manual type annotations are
710 \isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
714 \begin{isamarkuptext}%
715 \begin{matharray}{rcl}
716 \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
717 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
720 Axiomatic type classes are Isabelle/Pure's primitive
721 \emph{definitional} interface to type classes. For practical
722 applications, you should consider using classes
723 (cf.~\secref{sec:classes}) which provide high level interface.
726 'axclass' classdecl (axmdecl prop +)
728 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
734 \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
735 axiomatic type class as the intersection of existing classes, with
736 additional axioms holding. Class axioms may not contain more than
737 one type variable. The class axioms (with implicit sort constraints
738 added) are bound to the given names. Furthermore a class
739 introduction rule is generated (being bound as \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.
741 The ``class axioms'' (which are derived from the internal class
742 definition) are stored as theorems according to the given name
743 specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added
744 here. The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
746 \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and \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}} setup a goal stating a class
747 relation or type arity. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
748 the type classes involved. After finishing the proof, the theory
749 will be augmented by a type signature declaration corresponding to
750 the resulting theorem.
756 \isamarkupsection{Unrestricted overloading%
760 \begin{isamarkuptext}%
761 Isabelle/Pure's definitional schemes support certain forms of
762 overloading (see \secref{sec:consts}). At most occassions
763 overloading will be used in a Haskell-like fashion together with
764 type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
765 \secref{sec:class}). Sometimes low-level overloading is desirable.
766 The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
769 \begin{matharray}{rcl}
770 \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
775 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
780 \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}}
781 opens a theory target (cf.\ \secref{sec:target}) which allows to
782 specify constants with overloaded definitions. These are identified
783 by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to
784 constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances. The
785 definitions themselves are established using common specification
786 tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the
787 corresponding constants. The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
789 A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
790 the corresponding definition, which is occasionally useful for
791 exotic overloading. It is at the discretion of the user to avoid
792 malformed theory specifications!
798 \isamarkupsection{Incorporating ML code \label{sec:ML}%
802 \begin{isamarkuptext}%
803 \begin{matharray}{rcl}
804 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
805 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
806 \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
807 \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
808 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
809 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
813 \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
814 \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
820 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
826 \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML
827 commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
828 down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with
829 the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
830 header (see also \secref{sec:begin-thy}).
832 Top-level ML bindings are stored within the (global or local) theory
835 \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
836 but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
837 Top-level ML bindings are stored within the (global or local) theory
840 \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
841 within a proof context.
843 Top-level ML bindings are stored within the proof context in a
844 purely sequential fashion, disregarding the nested proof structure.
845 ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the
848 \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic
849 versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
850 updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML
851 toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
853 \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
854 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
855 of type \verb|theory -> theory|. This enables
856 to initialize any object-logic specific tools and packages written
859 \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
860 theorems produced in ML both in the theory context and the ML
861 toplevel, associating it with the provided name. Theorems are put
862 into a global ``standard'' format before being stored.
864 \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
871 \isamarkupsection{Primitive specification elements%
875 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
879 \begin{isamarkuptext}%
880 \begin{matharray}{rcll}
881 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
882 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
883 \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
884 \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
888 'classes' (classdecl +)
890 'classrel' (nameref ('<' | subseteq) nameref + 'and')
898 \item \hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}} declares class
899 \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.
900 Isabelle implicitly maintains the transitive closure of the class
901 hierarchy. Cyclic class structures are not permitted.
903 \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
904 relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
905 This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
906 (see \secref{sec:axclass}) provides a way to introduce proven class
909 \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
910 new default sort for any type variable that is given explicitly in
911 the text, but lacks a sort constraint (wrt.\ the current context).
912 Type variables generated by type inference are not affected.
914 Usually the default sort is only changed when defining a new
915 object-logic. For example, the default sort in Isabelle/HOL is
916 \isa{type}, the class of all HOL types. %FIXME sort antiq?
918 When merging theories, the default sorts of the parents are
919 logically intersected, i.e.\ the representations as lists of classes
922 \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation,
923 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
929 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
933 \begin{isamarkuptext}%
934 \begin{matharray}{rcll}
935 \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
936 \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
937 \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
941 'types' (typespec '=' type infix? +)
943 'typedecl' typespec infix?
945 'arities' (nameref '::' arity +)
951 \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}} introduces a
952 \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type
953 \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as are available in
954 Isabelle/HOL for example, type synonyms are merely syntactic
955 abbreviations without any logical significance. Internally, type
956 synonyms are fully expanded.
958 \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} declares a new
959 type constructor \isa{t}. If the object-logic defines a base sort
960 \isa{s}, then the constructor is declared to operate on that, via
961 the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.
963 \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
964 Isabelle's order-sorted signature of types by new type constructor
965 arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
966 command (see \secref{sec:axclass}) provides a way to introduce
973 \isamarkupsubsection{Co-regularity of type classes and arities%
977 \begin{isamarkuptext}%
978 The class relation together with the collection of
979 type-constructor arities must obey the principle of
980 \emph{co-regularity} as defined below.
982 \medskip For the subsequent formulation of co-regularity we assume
983 that the class relation is closed by transitivity and reflexivity.
984 Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is
985 completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}
986 implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.
988 Treating sorts as finite sets of classes (meaning the intersection),
989 the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as
992 \isa{{\isachardoublequote}s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlsub {\isadigit{2}}\ {\isasymequiv}\ {\isasymforall}c\isactrlsub {\isadigit{2}}\ {\isasymin}\ s\isactrlsub {\isadigit{2}}{\isachardot}\ {\isasymexists}c\isactrlsub {\isadigit{1}}\ {\isasymin}\ s\isactrlsub {\isadigit{1}}{\isachardot}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}
995 This relation on sorts is further extended to tuples of sorts (of
996 the same length) in the component-wise way.
998 \smallskip Co-regularity of the class relation together with the
999 arities relation means:
1001 \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{1}}{\isacharparenright}c\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{2}}{\isacharparenright}c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ \isactrlvec s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlsub {\isadigit{2}}{\isachardoublequote}}
1003 \noindent for all such arities. In other words, whenever the result
1004 classes of some type-constructor arities are related, then the
1005 argument sorts need to be related in the same way.
1007 \medskip Co-regularity is a very fundamental property of the
1008 order-sorted algebra of types. For example, it entails principle
1009 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
1010 \end{isamarkuptext}%
1013 \isamarkupsubsection{Constants and definitions \label{sec:consts}%
1017 \begin{isamarkuptext}%
1018 Definitions essentially express abbreviations within the logic. The
1019 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
1020 where the arguments of \isa{c} appear on the left, abbreviating a
1021 prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
1022 written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
1023 definitions may be weakened by adding arbitrary pre-conditions:
1024 \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
1026 \medskip The built-in well-formedness conditions for definitional
1031 \item Arguments (on the left-hand side) must be distinct variables.
1033 \item All variables on the right-hand side must also appear on the
1036 \item All type variables on the right-hand side must also appear on
1037 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.
1039 \item The definition must not be recursive. Most object-logics
1040 provide definitional principles that can be used to express
1045 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
1046 recursively at type instances corresponding to the immediate
1047 argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
1048 specification patterns impose global constraints on all occurrences,
1049 e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
1050 corresponding occurrences on some right-hand side need to be an
1051 instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
1053 \begin{matharray}{rcl}
1054 \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1055 \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1056 \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1060 'consts' ((name '::' type mixfix?) +)
1062 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1067 'constdefs' structs? (constdecl? constdef +)
1070 structs: '(' 'structure' (vars + 'and') ')'
1072 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1074 constdef: thmdecl? prop
1080 \item \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}} declares constant \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The optional
1081 mixfix annotations may attach concrete syntax to the constants
1084 \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}
1085 as a definitional axiom for some existing constant.
1087 The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
1088 for this definition, which is occasionally useful for exotic
1089 overloading. It is at the discretion of the user to avoid malformed
1090 theory specifications!
1092 The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
1093 potentially overloaded. Unless this option is given, a warning
1094 message would be issued for any definitional equation with a more
1095 special type than that of the corresponding constant declaration.
1097 \item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and
1098 definitions, with type-inference taking care of the most general
1099 typing of the given specification (the optional type constraint may
1100 refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The
1101 resulting type declaration needs to agree with that of the
1102 specification; overloading is \emph{not} supported here!
1104 The constant name may be omitted altogether, if neither type nor
1105 syntax declarations are given. The canonical name of the
1106 definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
1107 unless specified otherwise. Also note that the given list of
1108 specifications is processed in a strictly sequential manner, with
1109 type-checking being performed independently.
1111 An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
1112 admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
1113 particularly useful with locales (see also \secref{sec:locale}).
1116 \end{isamarkuptext}%
1119 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
1123 \begin{isamarkuptext}%
1124 \begin{matharray}{rcll}
1125 \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
1126 \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1127 \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1131 'axioms' (axmdecl prop +)
1133 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1139 \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary
1140 statements as axioms of the meta-logic. In fact, axioms are
1141 ``axiomatic theorems'', and may be referred later just as any other
1144 Axioms are usually only introduced when declaring new logical
1145 systems. Everyday work is typically done the hard way, with proper
1146 definitions and proven theorems.
1148 \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores
1149 existing facts in the theory context, or the specified target
1150 context (see also \secref{sec:target}). Typical applications would
1151 also involve attributes, to declare Simplifier rules, for example.
1153 \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.
1156 \end{isamarkuptext}%
1159 \isamarkupsection{Oracles%
1163 \begin{isamarkuptext}%
1164 Oracles allow Isabelle to take advantage of external reasoners
1165 such as arithmetic decision procedures, model checkers, fast
1166 tautology checkers or computer algebra systems. Invoked as an
1167 oracle, an external reasoner can create arbitrary Isabelle theorems.
1169 It is the responsibility of the user to ensure that the external
1170 reasoner is as trustworthy as the application requires. Another
1171 typical source of errors is the linkup between Isabelle and the
1172 external tool, not just its concrete implementation, but also the
1173 required translation between two different logical environments.
1175 Isabelle merely guarantees well-formedness of the propositions being
1176 asserted, and records within the internal derivation object how
1177 presumed theorems depend on unproven suppositions.
1179 \begin{matharray}{rcl}
1180 \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1184 'oracle' name '=' text
1190 \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML
1191 expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
1192 ML function of type \verb|'a -> thm|, which is bound to the
1193 global identifier \verb|name|. This acts like an infinitary
1194 specification of axioms! Invoking the oracle only works within the
1195 scope of the resulting theory.
1199 See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
1200 defining a new primitive rule as oracle, and turning it into a proof
1202 \end{isamarkuptext}%
1205 \isamarkupsection{Name spaces%
1209 \begin{isamarkuptext}%
1210 \begin{matharray}{rcl}
1211 \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1212 \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1213 \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1217 'hide' ('(open)')? name (nameref + )
1221 Isabelle organizes any kind of name declarations (of types,
1222 constants, theorems etc.) by separate hierarchically structured name
1223 spaces. Normally the user does not have to control the behavior of
1224 name spaces by hand, yet the following commands provide some way to
1229 \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
1230 name declaration mode. Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
1231 the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
1232 names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
1234 Note that global names are prone to get hidden accidently later,
1235 when qualified names of the same base name are introduced.
1237 \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
1238 declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
1239 \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
1240 (unqualified) names may never be hidden.
1242 Note that hiding name space accesses has no impact on logical
1243 declarations --- they remain valid internally. Entities that are no
1244 longer accessible to the user are printed with the special qualifier
1245 ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
1248 \end{isamarkuptext}%
1256 \isacommand{end}\isamarkupfalse%
1266 %%% Local Variables:
1268 %%% TeX-master: "root"