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' ('(pervasive)')? 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 If the \isa{{\isachardoublequote}{\isacharparenleft}pervasive{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
295 declaration is applied to all possible contexts involved, including
296 the global background theory.
298 \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
299 current local theory context. No theorem binding is involved here,
300 unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
301 \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
302 of applying attributes as included in the theorem specification.
308 \isamarkupsection{Locales \label{sec:locale}%
312 \begin{isamarkuptext}%
313 Locales are parametric named local contexts, consisting of a list of
314 declaration elements that are modeled after the Isar proof context
315 commands (cf.\ \secref{sec:proof-context}).%
319 \isamarkupsubsection{Locale expressions \label{sec:locale-expr}%
323 \begin{isamarkuptext}%
324 A \emph{locale expression} denotes a structured context composed of
325 instances of existing locales. The context consists of a list of
326 instances of declaration elements from the locales. Two locale
327 instances are equal if they are of the same locale and the
328 parameters are instantiated with equivalent terms. Declaration
329 elements from equal instances are never repeated, thus avoiding
330 duplicate declarations.
332 \indexouternonterm{localeexpr}
334 localeexpr: (instance + '+') ('for' (fixes + 'and'))?
336 instance: (qualifier ':')? nameref (posinsts | namedinsts)
338 qualifier: name ('?' | '!')?
340 posinsts: (term | '_')*
342 namedinsts: 'where' (name '=' term + 'and')
346 A locale instance consists of a reference to a locale and either
347 positional or named parameter instantiations. Identical
348 instantiations (that is, those that instante a parameter by itself)
349 may be omitted. The notation `\_' enables to omit the instantiation
350 for a parameter inside a positional instantiation.
352 Terms in instantiations are from the context the locale expressions
353 is declared in. Local names may be added to this context with the
354 optional for clause. In addition, syntax declarations from one
355 instance are effective when parsing subsequent instances of the same
358 Instances have an optional qualifier which applies to names in
359 declarations. Names include local definitions and theorem names.
360 If present, the qualifier itself is either optional
361 (``\texttt{?}''), which means that it may be omitted on input of the
362 qualified name, or mandatory (``\texttt{!}''). If neither
363 ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
364 is used. For \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}
365 the default is ``mandatory'', for \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} the default is ``optional''.%
369 \isamarkupsubsection{Locale declarations%
373 \begin{isamarkuptext}%
374 \begin{matharray}{rcl}
375 \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
376 \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}} \\
377 \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}} \\
378 \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isa{method} \\
379 \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\
382 \indexouternonterm{contextelem}
383 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
384 \indexisarelem{defines}\indexisarelem{notes}
386 'locale' name ('=' locale)? 'begin'?
388 'print\_locale' '!'? nameref
390 locale: contextelem+ | localeexpr ('+' (contextelem+))?
393 'fixes' (fixes + 'and')
394 | 'constrains' (name '::' type + 'and')
395 | 'assumes' (props + 'and')
396 | 'defines' (thmdecl? prop proppat? + 'and')
397 | 'notes' (thmdef? thmrefs + 'and')
403 \item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}} defines a
404 new locale \isa{loc} as a context consisting of a certain view of
405 existing locales (\isa{import}) plus some additional elements
406 (\isa{body}). Both \isa{import} and \isa{body} are optional;
407 the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
408 locale, which may still be useful to collect declarations of facts
409 later on. Type-inference on locale expressions automatically takes
410 care of the most general typing that the combined context elements
413 The \isa{import} consists of a structured locale expression; see
414 \secref{sec:proof-context} above. Its for clause defines the local
415 parameters of the \isa{import}. In addition, locale parameters
416 whose instantance is omitted automatically extend the (possibly
417 empty) for clause: they are inserted at its beginning. This means
418 that these parameters may be referred to from within the expression
419 and also in the subsequent context elements and provides a
420 notational convenience for the inheritance of parameters in locale
423 The \isa{body} consists of context elements.
427 \item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares a local
428 parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
429 are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
430 implicitly in this context.
432 \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type
433 constraint \isa{{\isasymtau}} on the local parameter \isa{x}. This
434 element is deprecated. The type constaint should be introduced in
435 the for clause or the relevant \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} element.
437 \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}
438 introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
439 proof (cf.\ \secref{sec:proof-context}).
441 \item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} defines a previously
442 declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
443 proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
444 takes an equational proposition instead of variable-term pair. The
445 left-hand side of the equation may have additional arguments, e.g.\
446 ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
448 \item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}
449 reconsiders facts within a local context. Most notably, this may
450 include arbitrary declarations in any attribute specifications
451 included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
453 The initial \isa{import} specification of a locale expression
454 maintains a dynamic relation to the locales being referenced
455 (benefiting from any later fact declarations in the obvious manner).
459 Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
460 in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
461 are illegal in locale definitions. In the long goal format of
462 \secref{sec:goals}, term bindings may be included as expected,
465 \medskip Locale specifications are ``closed up'' by
466 turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
467 (modulo local definitions). The predicate statement covers only the
468 newly specified assumptions, omitting the content of included locale
469 expressions. The full cumulative view is only provided on export,
470 involving another predicate \isa{loc} that refers to the complete
473 In any case, the predicate arguments are those locale parameters
474 that actually occur in the respective piece of text. Also note that
475 these predicates operate at the meta-level in theory, but the locale
476 packages attempts to internalize statements according to the
477 object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
478 \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
479 \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
481 \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
482 contents of the named locale. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
483 elements by default. Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
486 \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
487 of the current theory.
489 \item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}
490 repeatedly expand all introduction rules of locale predicates of the
491 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
492 assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
493 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
494 specifications entailed by the context, both from target statements,
495 and from interpretations (see below). New goals that are entailed
496 by the current context are discharged automatically.
502 \isamarkupsubsection{Locale interpretations%
506 \begin{isamarkuptext}%
507 Locale expressions may be instantiated, and the instantiated facts
508 added to the current context. This requires a proof of the
509 instantiated specification and is called \emph{locale
510 interpretation}. Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and
511 also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
513 \begin{matharray}{rcl}
514 \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
515 \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
516 \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
517 \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
520 \indexouternonterm{interp}
522 'sublocale' nameref ('<' | subseteq) localeexpr
524 'interpretation' localeepxr equations?
526 'interpret' localeexpr
528 'print\_interps' nameref
530 equations: 'where' (thmdecl? prop + 'and')
536 \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
537 interprets \isa{expr} in the locale \isa{name}. A proof that
538 the specification of \isa{name} implies the specification of
539 \isa{expr} is required. As in the localized version of the
540 theorem command, the proof is in the context of \isa{name}. After
541 the proof obligation has been dischared, the facts of \isa{expr}
542 become part of locale \isa{name} as \emph{derived} context
543 elements and are available when the context \isa{name} is
544 subsequently entered. Note that, like import, this is dynamic:
545 facts added to a locale part of \isa{expr} after interpretation
546 become also available in \isa{name}.
548 Only specification fragments of \isa{expr} that are not already
549 part of \isa{name} (be it imported, derived or a derived fragment
550 of the import) are considered in this process. This enables
551 circular interpretations to the extent that no infinite chains are
552 generated in the locale hierarchy.
554 If interpretations of \isa{name} exist in the current theory, the
555 command adds interpretations for \isa{expr} as well, with the same
556 qualifier, although only for fragments of \isa{expr} that are not
557 interpreted in the theory already.
559 \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
560 interprets \isa{expr} in the theory. The command generates proof
561 obligations for the instantiated specifications (assumes and defines
562 elements). Once these are discharged by the user, instantiated
563 facts are added to the theory in a post-processing phase.
565 Additional equations, which are unfolded during
566 post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
567 This is useful for interpreting concepts introduced through
568 definition specification elements. The equations must be proved.
570 The command is aware of interpretations already active in the
571 theory, but does not simplify the goal automatically. In order to
572 simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}
573 or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}. Post-processing is not applied to
574 facts of interpretations that are already active. This avoids
575 duplication of interpreted facts, in particular. Note that, in the
576 case of a locale with import, parts of the interpretation may
577 already be active. The command will only process facts for new
580 Adding facts to locales has the effect of adding interpreted facts
581 to the theory for all active interpretations also. That is,
582 interpretations dynamically participate in any facts added to
585 \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
586 interprets \isa{expr} in the proof context and is otherwise
587 similar to interpretation in theories.
589 \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
590 interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
591 those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
592 one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
597 Since attributes are applied to interpreted theorems,
598 interpretation may modify the context of common proof tools, e.g.\
599 the Simplifier or Classical Reasoner. As the behavior of such
600 tools is \emph{not} stable under interpretation morphisms, manual
601 declarations might have to be added to the target context of the
602 interpretation to revert such declarations.
606 An interpretation in a theory may subsume previous
607 interpretations. This happens if the same specification fragment
608 is interpreted twice and the instantiation of the second
609 interpretation is more general than the interpretation of the
610 first. The locale package does not attempt to remove subsumed
616 \isamarkupsection{Classes \label{sec:class}%
620 \begin{isamarkuptext}%
621 A class is a particular locale with \emph{exactly one} type variable
622 \isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
623 is established which is interpreted logically as axiomatic type
624 class \cite{Wenzel:1997:TPHOL} whose logical content are the
625 assumptions of the locale. Thus, classes provide the full
626 generality of locales combined with the commodity of type classes
627 (notably type-inference). See \cite{isabelle-classes} for a short
630 \begin{matharray}{rcl}
631 \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
632 \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
633 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
634 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
635 \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
636 \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}} \\
637 \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}} \\
638 \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\
642 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
645 'instantiation' (nameref + 'and') '::' arity 'begin'
649 'instance' (nameref + 'and') '::' arity
651 'subclass' target? nameref
653 'instance' nameref ('<' | subseteq) nameref
660 superclassexpr: nameref | (nameref '+' superclassexpr)
666 \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}} defines
667 a new class \isa{c}, inheriting from \isa{superclasses}. This
668 introduces a locale \isa{c} with import of all locales \isa{superclasses}.
670 Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
671 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
672 \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
674 Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
675 mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
676 corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
677 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
678 --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
679 class membership proofs.
681 \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
682 allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding
683 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
684 target body poses a goal stating these type arities. The target is
685 concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
687 Note that a list of simultaneous type constructors may be given;
688 this corresponds nicely to mutually recursive type definitions, e.g.\
691 \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
692 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
693 the type classes involved. After finishing the proof, the
694 background theory will be augmented by the proven type arities.
696 On the theory level, \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}} provides a convenient way to instantiate a type class with no
697 need to specifify operations: one can continue with the
698 instantiation proof immediately.
700 \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
701 \isa{d} sets up a goal stating that class \isa{c} is logically
702 contained in class \isa{d}. After finishing the proof, class
703 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
705 A weakend form of this is available through a further variant of
706 \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}: \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} opens
707 a proof that class \isa{{\isachardoublequote}c\isactrlisub {\isadigit{2}}{\isachardoublequote}} implies \isa{{\isachardoublequote}c\isactrlisub {\isadigit{1}}{\isachardoublequote}} without reference
708 to the underlying locales; this is useful if the properties to prove
709 the logical connection are not sufficent on the locale level but on
712 \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
715 \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes all classes and their
716 subclass relations as a Hasse diagram.
718 \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class
719 introduction rules of this theory. Note that this method usually
720 needs not be named explicitly, as it is already included in the
721 default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
722 instantiation of trivial (syntactic) classes may be performed by a
723 single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
729 \isamarkupsubsection{The class target%
733 \begin{isamarkuptext}%
736 A named context may refer to a locale (cf.\ \secref{sec:target}).
737 If this locale is also a class \isa{c}, apart from the common
738 locale target behaviour the following happens.
742 \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
743 local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
744 are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
745 referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
747 \item Local theorem bindings are lifted as are assumptions.
749 \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
750 global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
751 resolves ambiguities. In rare cases, manual type annotations are
758 \isamarkupsection{Unrestricted overloading%
762 \begin{isamarkuptext}%
763 Isabelle/Pure's definitional schemes support certain forms of
764 overloading (see \secref{sec:consts}). Overloading means that a
765 constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be
766 defined separately on type instances
767 \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}}
768 for each type constructor \isa{t}. At most occassions
769 overloading will be used in a Haskell-like fashion together with
770 type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
771 \secref{sec:class}). Sometimes low-level overloading is desirable.
772 The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
775 \begin{matharray}{rcl}
776 \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
781 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
786 \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}}
787 opens a theory target (cf.\ \secref{sec:target}) which allows to
788 specify constants with overloaded definitions. These are identified
789 by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to
790 constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances. The
791 definitions themselves are established using common specification
792 tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the
793 corresponding constants. The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
795 A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
796 the corresponding definition, which is occasionally useful for
797 exotic overloading (see \secref{sec:consts} for a precise description).
798 It is at the discretion of the user to avoid
799 malformed theory specifications!
805 \isamarkupsection{Incorporating ML code \label{sec:ML}%
809 \begin{isamarkuptext}%
810 \begin{matharray}{rcl}
811 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
812 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
813 \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
814 \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
815 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
816 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
817 \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
818 \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
822 \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
823 \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
829 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
831 'attribute\_setup' name '=' text text
837 \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML
838 commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
839 down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with
840 the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
841 header (see also \secref{sec:begin-thy}).
843 Top-level ML bindings are stored within the (global or local) theory
846 \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
847 but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
848 Top-level ML bindings are stored within the (global or local) theory
851 \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
852 within a proof context.
854 Top-level ML bindings are stored within the proof context in a
855 purely sequential fashion, disregarding the nested proof structure.
856 ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the
859 \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic
860 versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
861 updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML
862 toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
864 \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
865 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
866 of type \verb|theory -> theory|. This enables to initialize
867 any object-logic specific tools and packages written in ML, for
870 \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
871 a local theory context, and an ML expression of type \verb|local_theory -> local_theory|. This allows to
872 invoke local theory specification packages without going through
873 concrete outer syntax, for example.
875 \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
876 defines an attribute in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
877 \verb|attribute context_parser|, cf.\ basic parsers defined in
878 structure \verb|Args| and \verb|Attrib|.
880 In principle, attributes can operate both on a given theorem and the
881 implicit context, although in practice only one is modified and the
882 other serves as parameter. Here are examples for these two cases:
893 \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
894 \ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
895 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
896 \ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
897 \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
898 \ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
900 \ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
901 \ my{\isacharunderscore}declaration\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
902 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
903 \ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
904 \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
905 \ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
913 \begin{isamarkuptext}%
916 \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
917 theorems produced in ML both in the theory context and the ML
918 toplevel, associating it with the provided name. Theorems are put
919 into a global ``standard'' format before being stored.
921 \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
928 \isamarkupsection{Primitive specification elements%
932 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
936 \begin{isamarkuptext}%
937 \begin{matharray}{rcll}
938 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
939 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
940 \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
941 \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}} \\
945 'classes' (classdecl +)
947 'classrel' (nameref ('<' | subseteq) nameref + 'and')
955 \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
956 \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.
957 Isabelle implicitly maintains the transitive closure of the class
958 hierarchy. Cyclic class structures are not permitted.
960 \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
961 relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
962 This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
963 and \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} command
964 (see \secref{sec:class}) provide a way to introduce proven class
967 \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
968 new default sort for any type variable that is given explicitly in
969 the text, but lacks a sort constraint (wrt.\ the current context).
970 Type variables generated by type inference are not affected.
972 Usually the default sort is only changed when defining a new
973 object-logic. For example, the default sort in Isabelle/HOL is
974 \isa{type}, the class of all HOL types. %FIXME sort antiq?
976 When merging theories, the default sorts of the parents are
977 logically intersected, i.e.\ the representations as lists of classes
980 \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation,
981 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
987 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
991 \begin{isamarkuptext}%
992 \begin{matharray}{rcll}
993 \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
994 \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
995 \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
999 'types' (typespec '=' type mixfix? +)
1001 'typedecl' typespec mixfix?
1003 'arities' (nameref '::' arity +)
1009 \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
1010 \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type
1011 \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as are available in
1012 Isabelle/HOL for example, type synonyms are merely syntactic
1013 abbreviations without any logical significance. Internally, type
1014 synonyms are fully expanded.
1016 \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
1017 type constructor \isa{t}. If the object-logic defines a base sort
1018 \isa{s}, then the constructor is declared to operate on that, via
1019 the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.
1021 \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
1022 Isabelle's order-sorted signature of types by new type constructor
1023 arities. This is done axiomatically! The \indexref{}{command}{instantiation}\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
1024 target (see \secref{sec:class}) provides a way to introduce
1025 proven type arities.
1028 \end{isamarkuptext}%
1031 \isamarkupsubsection{Co-regularity of type classes and arities%
1035 \begin{isamarkuptext}%
1036 The class relation together with the collection of
1037 type-constructor arities must obey the principle of
1038 \emph{co-regularity} as defined below.
1040 \medskip For the subsequent formulation of co-regularity we assume
1041 that the class relation is closed by transitivity and reflexivity.
1042 Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is
1043 completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}
1044 implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.
1046 Treating sorts as finite sets of classes (meaning the intersection),
1047 the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as
1050 \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}}
1053 This relation on sorts is further extended to tuples of sorts (of
1054 the same length) in the component-wise way.
1056 \smallskip Co-regularity of the class relation together with the
1057 arities relation means:
1059 \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}}
1061 \noindent for all such arities. In other words, whenever the result
1062 classes of some type-constructor arities are related, then the
1063 argument sorts need to be related in the same way.
1065 \medskip Co-regularity is a very fundamental property of the
1066 order-sorted algebra of types. For example, it entails principle
1067 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
1068 \end{isamarkuptext}%
1071 \isamarkupsubsection{Constants and definitions \label{sec:consts}%
1075 \begin{isamarkuptext}%
1076 Definitions essentially express abbreviations within the logic. The
1077 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
1078 where the arguments of \isa{c} appear on the left, abbreviating a
1079 prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
1080 written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
1081 definitions may be weakened by adding arbitrary pre-conditions:
1082 \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
1084 \medskip The built-in well-formedness conditions for definitional
1089 \item Arguments (on the left-hand side) must be distinct variables.
1091 \item All variables on the right-hand side must also appear on the
1094 \item All type variables on the right-hand side must also appear on
1095 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.
1097 \item The definition must not be recursive. Most object-logics
1098 provide definitional principles that can be used to express
1103 The right-hand side of overloaded definitions may mention overloaded constants
1104 recursively at type instances corresponding to the immediate
1105 argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
1106 specification patterns impose global constraints on all occurrences,
1107 e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
1108 corresponding occurrences on some right-hand side need to be an
1109 instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
1111 \begin{matharray}{rcl}
1112 \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1113 \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1114 \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1118 'consts' ((name '::' type mixfix?) +)
1120 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1125 'constdefs' structs? (constdecl? constdef +)
1128 structs: '(' 'structure' (vars + 'and') ')'
1130 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1132 constdef: thmdecl? prop
1138 \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
1139 mixfix annotations may attach concrete syntax to the constants
1142 \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}
1143 as a definitional axiom for some existing constant.
1145 The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
1146 for this definition, which is occasionally useful for exotic
1147 overloading. It is at the discretion of the user to avoid malformed
1148 theory specifications!
1150 The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
1151 potentially overloaded. Unless this option is given, a warning
1152 message would be issued for any definitional equation with a more
1153 special type than that of the corresponding constant declaration.
1155 \item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and
1156 definitions, with type-inference taking care of the most general
1157 typing of the given specification (the optional type constraint may
1158 refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The
1159 resulting type declaration needs to agree with that of the
1160 specification; overloading is \emph{not} supported here!
1162 The constant name may be omitted altogether, if neither type nor
1163 syntax declarations are given. The canonical name of the
1164 definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
1165 unless specified otherwise. Also note that the given list of
1166 specifications is processed in a strictly sequential manner, with
1167 type-checking being performed independently.
1169 An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
1170 admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
1171 particularly useful with locales (see also \secref{sec:locale}).
1174 \end{isamarkuptext}%
1177 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
1181 \begin{isamarkuptext}%
1182 \begin{matharray}{rcll}
1183 \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
1184 \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1185 \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1189 'axioms' (axmdecl prop +)
1191 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1197 \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary
1198 statements as axioms of the meta-logic. In fact, axioms are
1199 ``axiomatic theorems'', and may be referred later just as any other
1202 Axioms are usually only introduced when declaring new logical
1203 systems. Everyday work is typically done the hard way, with proper
1204 definitions and proven theorems.
1206 \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores
1207 existing facts in the theory context, or the specified target
1208 context (see also \secref{sec:target}). Typical applications would
1209 also involve attributes, to declare Simplifier rules, for example.
1211 \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.
1214 \end{isamarkuptext}%
1217 \isamarkupsection{Oracles%
1221 \begin{isamarkuptext}%
1222 Oracles allow Isabelle to take advantage of external reasoners
1223 such as arithmetic decision procedures, model checkers, fast
1224 tautology checkers or computer algebra systems. Invoked as an
1225 oracle, an external reasoner can create arbitrary Isabelle theorems.
1227 It is the responsibility of the user to ensure that the external
1228 reasoner is as trustworthy as the application requires. Another
1229 typical source of errors is the linkup between Isabelle and the
1230 external tool, not just its concrete implementation, but also the
1231 required translation between two different logical environments.
1233 Isabelle merely guarantees well-formedness of the propositions being
1234 asserted, and records within the internal derivation object how
1235 presumed theorems depend on unproven suppositions.
1237 \begin{matharray}{rcl}
1238 \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1242 'oracle' name '=' text
1248 \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML
1249 expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
1250 ML function of type \verb|'a -> thm|, which is bound to the
1251 global identifier \verb|name|. This acts like an infinitary
1252 specification of axioms! Invoking the oracle only works within the
1253 scope of the resulting theory.
1257 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
1258 defining a new primitive rule as oracle, and turning it into a proof
1260 \end{isamarkuptext}%
1263 \isamarkupsection{Name spaces%
1267 \begin{isamarkuptext}%
1268 \begin{matharray}{rcl}
1269 \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1270 \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1271 \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1275 'hide' ('(open)')? name (nameref + )
1279 Isabelle organizes any kind of name declarations (of types,
1280 constants, theorems etc.) by separate hierarchically structured name
1281 spaces. Normally the user does not have to control the behavior of
1282 name spaces by hand, yet the following commands provide some way to
1287 \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
1288 name declaration mode. Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
1289 the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
1290 names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
1292 Note that global names are prone to get hidden accidently later,
1293 when qualified names of the same base name are introduced.
1295 \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
1296 declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
1297 \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
1298 (unqualified) names may never be hidden.
1300 Note that hiding name space accesses has no impact on logical
1301 declarations --- they remain valid internally. Entities that are no
1302 longer accessible to the user are printed with the special qualifier
1303 ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
1306 \end{isamarkuptext}%
1314 \isacommand{end}\isamarkupfalse%
1324 %%% Local Variables:
1326 %%% TeX-master: "root"