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 constraint 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 equations?
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\ {\isasymWHERE}\ eqns{\isachardoublequote}} interprets
586 \isa{expr} in the proof context and is otherwise similar to
587 interpretation in theories. Note that rewrite rules given to
588 \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} should be explicitly universally quantified.
590 \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
591 interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory or proof
592 context, including those due to a combination of a \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} or \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} and one or several
593 \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
598 Since attributes are applied to interpreted theorems,
599 interpretation may modify the context of common proof tools, e.g.\
600 the Simplifier or Classical Reasoner. As the behavior of such
601 tools is \emph{not} stable under interpretation morphisms, manual
602 declarations might have to be added to the target context of the
603 interpretation to revert such declarations.
607 An interpretation in a theory or proof context may subsume previous
608 interpretations. This happens if the same specification fragment
609 is interpreted twice and the instantiation of the second
610 interpretation is more general than the interpretation of the
611 first. The locale package does not attempt to remove subsumed
617 \isamarkupsection{Classes \label{sec:class}%
621 \begin{isamarkuptext}%
622 A class is a particular locale with \emph{exactly one} type variable
623 \isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
624 is established which is interpreted logically as axiomatic type
625 class \cite{Wenzel:1997:TPHOL} whose logical content are the
626 assumptions of the locale. Thus, classes provide the full
627 generality of locales combined with the commodity of type classes
628 (notably type-inference). See \cite{isabelle-classes} for a short
631 \begin{matharray}{rcl}
632 \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
633 \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
634 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
635 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
636 \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
637 \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}} \\
638 \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}} \\
639 \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\
643 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
646 'instantiation' (nameref + 'and') '::' arity 'begin'
650 'instance' (nameref + 'and') '::' arity
652 'subclass' target? nameref
654 'instance' nameref ('<' | subseteq) nameref
661 superclassexpr: nameref | (nameref '+' superclassexpr)
667 \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}} defines
668 a new class \isa{c}, inheriting from \isa{superclasses}. This
669 introduces a locale \isa{c} with import of all locales \isa{superclasses}.
671 Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
672 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
673 \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
675 Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
676 mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
677 corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
678 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
679 --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
680 class membership proofs.
682 \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
683 allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding
684 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
685 target body poses a goal stating these type arities. The target is
686 concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
688 Note that a list of simultaneous type constructors may be given;
689 this corresponds nicely to mutually recursive type definitions, e.g.\
692 \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
693 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
694 the type classes involved. After finishing the proof, the
695 background theory will be augmented by the proven type arities.
697 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
698 need to specify operations: one can continue with the
699 instantiation proof immediately.
701 \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
702 \isa{d} sets up a goal stating that class \isa{c} is logically
703 contained in class \isa{d}. After finishing the proof, class
704 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
706 A weakend form of this is available through a further variant of
707 \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
708 a proof that class \isa{{\isachardoublequote}c\isactrlisub {\isadigit{2}}{\isachardoublequote}} implies \isa{{\isachardoublequote}c\isactrlisub {\isadigit{1}}{\isachardoublequote}} without reference
709 to the underlying locales; this is useful if the properties to prove
710 the logical connection are not sufficent on the locale level but on
713 \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
716 \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes all classes and their
717 subclass relations as a Hasse diagram.
719 \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class
720 introduction rules of this theory. Note that this method usually
721 needs not be named explicitly, as it is already included in the
722 default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
723 instantiation of trivial (syntactic) classes may be performed by a
724 single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
730 \isamarkupsubsection{The class target%
734 \begin{isamarkuptext}%
737 A named context may refer to a locale (cf.\ \secref{sec:target}).
738 If this locale is also a class \isa{c}, apart from the common
739 locale target behaviour the following happens.
743 \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
744 local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
745 are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
746 referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
748 \item Local theorem bindings are lifted as are assumptions.
750 \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
751 global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
752 resolves ambiguities. In rare cases, manual type annotations are
759 \isamarkupsubsection{Co-regularity of type classes and arities%
763 \begin{isamarkuptext}%
764 The class relation together with the collection of
765 type-constructor arities must obey the principle of
766 \emph{co-regularity} as defined below.
768 \medskip For the subsequent formulation of co-regularity we assume
769 that the class relation is closed by transitivity and reflexivity.
770 Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is
771 completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}
772 implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.
774 Treating sorts as finite sets of classes (meaning the intersection),
775 the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as
778 \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}}
781 This relation on sorts is further extended to tuples of sorts (of
782 the same length) in the component-wise way.
784 \smallskip Co-regularity of the class relation together with the
785 arities relation means:
787 \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}}
789 \noindent for all such arities. In other words, whenever the result
790 classes of some type-constructor arities are related, then the
791 argument sorts need to be related in the same way.
793 \medskip Co-regularity is a very fundamental property of the
794 order-sorted algebra of types. For example, it entails principle
795 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
799 \isamarkupsection{Unrestricted overloading%
803 \begin{isamarkuptext}%
804 Isabelle/Pure's definitional schemes support certain forms of
805 overloading (see \secref{sec:consts}). Overloading means that a
806 constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be
807 defined separately on type instances
808 \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}}
809 for each type constructor \isa{t}. At most occassions
810 overloading will be used in a Haskell-like fashion together with
811 type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
812 \secref{sec:class}). Sometimes low-level overloading is desirable.
813 The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
816 \begin{matharray}{rcl}
817 \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
822 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
827 \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}}
828 opens a theory target (cf.\ \secref{sec:target}) which allows to
829 specify constants with overloaded definitions. These are identified
830 by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to
831 constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances. The
832 definitions themselves are established using common specification
833 tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the
834 corresponding constants. The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
836 A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
837 the corresponding definition, which is occasionally useful for
838 exotic overloading (see \secref{sec:consts} for a precise description).
839 It is at the discretion of the user to avoid
840 malformed theory specifications!
846 \isamarkupsection{Incorporating ML code \label{sec:ML}%
850 \begin{isamarkuptext}%
851 \begin{matharray}{rcl}
852 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
853 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
854 \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
855 \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
856 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
857 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
858 \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}} \\
859 \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
865 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
867 'attribute\_setup' name '=' text text
873 \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML
874 commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
875 down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with
876 the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
877 header (see also \secref{sec:begin-thy}).
879 Top-level ML bindings are stored within the (global or local) theory
882 \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
883 but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
884 Top-level ML bindings are stored within the (global or local) theory
887 \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
888 within a proof context.
890 Top-level ML bindings are stored within the proof context in a
891 purely sequential fashion, disregarding the nested proof structure.
892 ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the
895 \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic
896 versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
897 updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML
898 toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
900 \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
901 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
902 of type \verb|theory -> theory|. This enables to initialize
903 any object-logic specific tools and packages written in ML, for
906 \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
907 a local theory context, and an ML expression of type \verb|local_theory -> local_theory|. This allows to
908 invoke local theory specification packages without going through
909 concrete outer syntax, for example.
911 \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
912 defines an attribute in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
913 \verb|attribute context_parser|, cf.\ basic parsers defined in
914 structure \verb|Args| and \verb|Attrib|.
916 In principle, attributes can operate both on a given theorem and the
917 implicit context, although in practice only one is modified and the
918 other serves as parameter. Here are examples for these two cases:
929 \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
930 \ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
931 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
932 \ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
933 \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
934 \ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
936 \ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
937 \ my{\isacharunderscore}declaration\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
938 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
939 \ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
940 \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
941 \ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
949 \isamarkupsection{Primitive specification elements%
953 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
957 \begin{isamarkuptext}%
958 \begin{matharray}{rcll}
959 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
960 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
961 \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}}
965 'classes' (classdecl +)
967 'classrel' (nameref ('<' | subseteq) nameref + 'and')
975 \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
976 \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.
977 Isabelle implicitly maintains the transitive closure of the class
978 hierarchy. Cyclic class structures are not permitted.
980 \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
981 relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
982 This is done axiomatically! The \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} and
983 \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} commands (see \secref{sec:class}) provide
984 a way to introduce proven class relations.
986 \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the
987 new default sort for any type variable that is given explicitly in
988 the text, but lacks a sort constraint (wrt.\ the current context).
989 Type variables generated by type inference are not affected.
991 Usually the default sort is only changed when defining a new
992 object-logic. For example, the default sort in Isabelle/HOL is
993 \isa{type}, the class of all HOL types.
995 When merging theories, the default sorts of the parents are
996 logically intersected, i.e.\ the representations as lists of classes
1000 \end{isamarkuptext}%
1003 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
1007 \begin{isamarkuptext}%
1008 \begin{matharray}{rcll}
1009 \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1010 \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1011 \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
1015 'types' (typespec '=' type mixfix? +)
1017 'typedecl' typespec mixfix?
1019 'arities' (nameref '::' arity +)
1025 \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
1026 \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type
1027 \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as are available in
1028 Isabelle/HOL for example, type synonyms are merely syntactic
1029 abbreviations without any logical significance. Internally, type
1030 synonyms are fully expanded.
1032 \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
1033 type constructor \isa{t}. If the object-logic defines a base sort
1034 \isa{s}, then the constructor is declared to operate on that, via
1035 the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.
1037 \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
1038 Isabelle's order-sorted signature of types by new type constructor
1039 arities. This is done axiomatically! The \indexref{}{command}{instantiation}\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
1040 target (see \secref{sec:class}) provides a way to introduce
1041 proven type arities.
1044 \end{isamarkuptext}%
1047 \isamarkupsubsection{Constants and definitions \label{sec:consts}%
1051 \begin{isamarkuptext}%
1052 Definitions essentially express abbreviations within the logic. The
1053 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
1054 where the arguments of \isa{c} appear on the left, abbreviating a
1055 prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
1056 written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
1057 definitions may be weakened by adding arbitrary pre-conditions:
1058 \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
1060 \medskip The built-in well-formedness conditions for definitional
1065 \item Arguments (on the left-hand side) must be distinct variables.
1067 \item All variables on the right-hand side must also appear on the
1070 \item All type variables on the right-hand side must also appear on
1071 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.
1073 \item The definition must not be recursive. Most object-logics
1074 provide definitional principles that can be used to express
1079 The right-hand side of overloaded definitions may mention overloaded constants
1080 recursively at type instances corresponding to the immediate
1081 argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
1082 specification patterns impose global constraints on all occurrences,
1083 e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
1084 corresponding occurrences on some right-hand side need to be an
1085 instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
1087 \begin{matharray}{rcl}
1088 \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1089 \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1093 'consts' ((name '::' type mixfix?) +)
1095 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1101 \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
1102 mixfix annotations may attach concrete syntax to the constants
1105 \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}
1106 as a definitional axiom for some existing constant.
1108 The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
1109 for this definition, which is occasionally useful for exotic
1110 overloading. It is at the discretion of the user to avoid malformed
1111 theory specifications!
1113 The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
1114 potentially overloaded. Unless this option is given, a warning
1115 message would be issued for any definitional equation with a more
1116 special type than that of the corresponding constant declaration.
1119 \end{isamarkuptext}%
1122 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
1126 \begin{isamarkuptext}%
1127 \begin{matharray}{rcll}
1128 \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
1129 \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1130 \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1134 'axioms' (axmdecl prop +)
1136 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1142 \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary
1143 statements as axioms of the meta-logic. In fact, axioms are
1144 ``axiomatic theorems'', and may be referred later just as any other
1147 Axioms are usually only introduced when declaring new logical
1148 systems. Everyday work is typically done the hard way, with proper
1149 definitions and proven theorems.
1151 \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores
1152 existing facts in the theory context, or the specified target
1153 context (see also \secref{sec:target}). Typical applications would
1154 also involve attributes, to declare Simplifier rules, for example.
1156 \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.
1159 \end{isamarkuptext}%
1162 \isamarkupsection{Oracles%
1166 \begin{isamarkuptext}%
1167 Oracles allow Isabelle to take advantage of external reasoners
1168 such as arithmetic decision procedures, model checkers, fast
1169 tautology checkers or computer algebra systems. Invoked as an
1170 oracle, an external reasoner can create arbitrary Isabelle theorems.
1172 It is the responsibility of the user to ensure that the external
1173 reasoner is as trustworthy as the application requires. Another
1174 typical source of errors is the linkup between Isabelle and the
1175 external tool, not just its concrete implementation, but also the
1176 required translation between two different logical environments.
1178 Isabelle merely guarantees well-formedness of the propositions being
1179 asserted, and records within the internal derivation object how
1180 presumed theorems depend on unproven suppositions.
1182 \begin{matharray}{rcl}
1183 \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1187 'oracle' name '=' text
1193 \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML
1194 expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
1195 ML function of type \verb|'a -> thm|, which is bound to the
1196 global identifier \verb|name|. This acts like an infinitary
1197 specification of axioms! Invoking the oracle only works within the
1198 scope of the resulting theory.
1202 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
1203 defining a new primitive rule as oracle, and turning it into a proof
1205 \end{isamarkuptext}%
1208 \isamarkupsection{Name spaces%
1212 \begin{isamarkuptext}%
1213 \begin{matharray}{rcl}
1214 \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1215 \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1216 \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1217 \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1221 ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
1225 Isabelle organizes any kind of name declarations (of types,
1226 constants, theorems etc.) by separate hierarchically structured name
1227 spaces. Normally the user does not have to control the behavior of
1228 name spaces by hand, yet the following commands provide some way to
1233 \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
1234 declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
1235 option, only the base name is hidden.
1237 Note that hiding name space accesses has no impact on logical
1238 declarations --- they remain valid internally. Entities that are no
1239 longer accessible to the user are printed with the special qualifier
1240 ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
1242 \item \hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}, \hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}, and \hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}} are similar to \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}, but hide types,
1243 constants, and facts, respectively.
1246 \end{isamarkuptext}%
1254 \isacommand{end}\isamarkupfalse%
1264 %%% Local Variables:
1266 %%% TeX-master: "root"