Generated files.
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 \isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
762 \begin{isamarkuptext}%
763 \begin{matharray}{rcl}
764 \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
767 Axiomatic type classes are Isabelle/Pure's primitive
768 interface to type classes. For practical
769 applications, you should consider using classes
770 (cf.~\secref{sec:classes}) which provide high level interface.
773 'axclass' classdecl (axmdecl prop +)
779 \item \hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}} defines an
780 axiomatic type class as the intersection of existing classes, with
781 additional axioms holding. Class axioms may not contain more than
782 one type variable. The class axioms (with implicit sort constraints
783 added) are bound to the given names. Furthermore a class
784 introduction rule is generated (being bound as \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
786 The ``class axioms'' (which are derived from the internal class
787 definition) are stored as theorems according to the given name
788 specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added
789 here. The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
795 \isamarkupsection{Unrestricted overloading%
799 \begin{isamarkuptext}%
800 Isabelle/Pure's definitional schemes support certain forms of
801 overloading (see \secref{sec:consts}). Overloading means that a
802 constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be
803 defined separately on type instances
804 \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}}
805 for each type constructor \isa{t}. At most occassions
806 overloading will be used in a Haskell-like fashion together with
807 type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
808 \secref{sec:class}). Sometimes low-level overloading is desirable.
809 The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
812 \begin{matharray}{rcl}
813 \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
818 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
823 \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}}
824 opens a theory target (cf.\ \secref{sec:target}) which allows to
825 specify constants with overloaded definitions. These are identified
826 by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to
827 constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances. The
828 definitions themselves are established using common specification
829 tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the
830 corresponding constants. The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
832 A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
833 the corresponding definition, which is occasionally useful for
834 exotic overloading (see \secref{sec:consts} for a precise description).
835 It is at the discretion of the user to avoid
836 malformed theory specifications!
842 \isamarkupsection{Incorporating ML code \label{sec:ML}%
846 \begin{isamarkuptext}%
847 \begin{matharray}{rcl}
848 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
849 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
850 \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
851 \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
852 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
853 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
854 \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}} \\
855 \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
859 \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
860 \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
866 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
868 'attribute\_setup' name '=' text text
874 \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML
875 commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
876 down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with
877 the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
878 header (see also \secref{sec:begin-thy}).
880 Top-level ML bindings are stored within the (global or local) theory
883 \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
884 but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
885 Top-level ML bindings are stored within the (global or local) theory
888 \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
889 within a proof context.
891 Top-level ML bindings are stored within the proof context in a
892 purely sequential fashion, disregarding the nested proof structure.
893 ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the
896 \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic
897 versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
898 updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML
899 toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
901 \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
902 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
903 of type \verb|theory -> theory|. This enables to initialize
904 any object-logic specific tools and packages written in ML, for
907 \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
908 a local theory context, and an ML expression of type \verb|local_theory -> local_theory|. This allows to
909 invoke local theory specification packages without going through
910 concrete outer syntax, for example.
912 \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
913 defines an attribute in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
914 \verb|attribute context_parser|, cf.\ basic parsers defined in
915 structure \verb|Args| and \verb|Attrib|.
917 In principle, attributes can operate both on a given theorem and the
918 implicit context, although in practice only one is modified and the
919 other serves as parameter. Here are examples for these two cases:
930 \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
931 \ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
932 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
933 \ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
934 \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
935 \ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
937 \ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
938 \ my{\isacharunderscore}declaration\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
939 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
940 \ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
941 \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
942 \ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
950 \begin{isamarkuptext}%
953 \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
954 theorems produced in ML both in the theory context and the ML
955 toplevel, associating it with the provided name. Theorems are put
956 into a global ``standard'' format before being stored.
958 \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
965 \isamarkupsection{Primitive specification elements%
969 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
973 \begin{isamarkuptext}%
974 \begin{matharray}{rcll}
975 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
976 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
977 \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
978 \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}} \\
982 'classes' (classdecl +)
984 'classrel' (nameref ('<' | subseteq) nameref + 'and')
992 \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
993 \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.
994 Isabelle implicitly maintains the transitive closure of the class
995 hierarchy. Cyclic class structures are not permitted.
997 \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
998 relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
999 This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
1000 (see \secref{sec:axclass}) provides a way to introduce proven class
1003 \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
1004 new default sort for any type variable that is given explicitly in
1005 the text, but lacks a sort constraint (wrt.\ the current context).
1006 Type variables generated by type inference are not affected.
1008 Usually the default sort is only changed when defining a new
1009 object-logic. For example, the default sort in Isabelle/HOL is
1010 \isa{type}, the class of all HOL types. %FIXME sort antiq?
1012 When merging theories, the default sorts of the parents are
1013 logically intersected, i.e.\ the representations as lists of classes
1016 \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation,
1017 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
1020 \end{isamarkuptext}%
1023 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
1027 \begin{isamarkuptext}%
1028 \begin{matharray}{rcll}
1029 \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1030 \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1031 \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
1035 'types' (typespec '=' type infix? +)
1037 'typedecl' typespec infix?
1039 'arities' (nameref '::' arity +)
1045 \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
1046 \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type
1047 \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as are available in
1048 Isabelle/HOL for example, type synonyms are merely syntactic
1049 abbreviations without any logical significance. Internally, type
1050 synonyms are fully expanded.
1052 \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
1053 type constructor \isa{t}. If the object-logic defines a base sort
1054 \isa{s}, then the constructor is declared to operate on that, via
1055 the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.
1057 \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
1058 Isabelle's order-sorted signature of types by new type constructor
1059 arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
1060 command (see \secref{sec:axclass}) provides a way to introduce
1061 proven type arities.
1064 \end{isamarkuptext}%
1067 \isamarkupsubsection{Co-regularity of type classes and arities%
1071 \begin{isamarkuptext}%
1072 The class relation together with the collection of
1073 type-constructor arities must obey the principle of
1074 \emph{co-regularity} as defined below.
1076 \medskip For the subsequent formulation of co-regularity we assume
1077 that the class relation is closed by transitivity and reflexivity.
1078 Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is
1079 completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}
1080 implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.
1082 Treating sorts as finite sets of classes (meaning the intersection),
1083 the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as
1086 \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}}
1089 This relation on sorts is further extended to tuples of sorts (of
1090 the same length) in the component-wise way.
1092 \smallskip Co-regularity of the class relation together with the
1093 arities relation means:
1095 \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}}
1097 \noindent for all such arities. In other words, whenever the result
1098 classes of some type-constructor arities are related, then the
1099 argument sorts need to be related in the same way.
1101 \medskip Co-regularity is a very fundamental property of the
1102 order-sorted algebra of types. For example, it entails principle
1103 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
1104 \end{isamarkuptext}%
1107 \isamarkupsubsection{Constants and definitions \label{sec:consts}%
1111 \begin{isamarkuptext}%
1112 Definitions essentially express abbreviations within the logic. The
1113 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
1114 where the arguments of \isa{c} appear on the left, abbreviating a
1115 prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
1116 written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
1117 definitions may be weakened by adding arbitrary pre-conditions:
1118 \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
1120 \medskip The built-in well-formedness conditions for definitional
1125 \item Arguments (on the left-hand side) must be distinct variables.
1127 \item All variables on the right-hand side must also appear on the
1130 \item All type variables on the right-hand side must also appear on
1131 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.
1133 \item The definition must not be recursive. Most object-logics
1134 provide definitional principles that can be used to express
1139 The right-hand side of overloaded definitions may mention overloaded constants
1140 recursively at type instances corresponding to the immediate
1141 argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
1142 specification patterns impose global constraints on all occurrences,
1143 e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
1144 corresponding occurrences on some right-hand side need to be an
1145 instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
1147 \begin{matharray}{rcl}
1148 \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1149 \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1150 \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1154 'consts' ((name '::' type mixfix?) +)
1156 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1161 'constdefs' structs? (constdecl? constdef +)
1164 structs: '(' 'structure' (vars + 'and') ')'
1166 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1168 constdef: thmdecl? prop
1174 \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
1175 mixfix annotations may attach concrete syntax to the constants
1178 \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}
1179 as a definitional axiom for some existing constant.
1181 The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
1182 for this definition, which is occasionally useful for exotic
1183 overloading. It is at the discretion of the user to avoid malformed
1184 theory specifications!
1186 The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
1187 potentially overloaded. Unless this option is given, a warning
1188 message would be issued for any definitional equation with a more
1189 special type than that of the corresponding constant declaration.
1191 \item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and
1192 definitions, with type-inference taking care of the most general
1193 typing of the given specification (the optional type constraint may
1194 refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The
1195 resulting type declaration needs to agree with that of the
1196 specification; overloading is \emph{not} supported here!
1198 The constant name may be omitted altogether, if neither type nor
1199 syntax declarations are given. The canonical name of the
1200 definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
1201 unless specified otherwise. Also note that the given list of
1202 specifications is processed in a strictly sequential manner, with
1203 type-checking being performed independently.
1205 An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
1206 admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
1207 particularly useful with locales (see also \secref{sec:locale}).
1210 \end{isamarkuptext}%
1213 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
1217 \begin{isamarkuptext}%
1218 \begin{matharray}{rcll}
1219 \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
1220 \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1221 \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
1225 'axioms' (axmdecl prop +)
1227 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1233 \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary
1234 statements as axioms of the meta-logic. In fact, axioms are
1235 ``axiomatic theorems'', and may be referred later just as any other
1238 Axioms are usually only introduced when declaring new logical
1239 systems. Everyday work is typically done the hard way, with proper
1240 definitions and proven theorems.
1242 \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores
1243 existing facts in the theory context, or the specified target
1244 context (see also \secref{sec:target}). Typical applications would
1245 also involve attributes, to declare Simplifier rules, for example.
1247 \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.
1250 \end{isamarkuptext}%
1253 \isamarkupsection{Oracles%
1257 \begin{isamarkuptext}%
1258 Oracles allow Isabelle to take advantage of external reasoners
1259 such as arithmetic decision procedures, model checkers, fast
1260 tautology checkers or computer algebra systems. Invoked as an
1261 oracle, an external reasoner can create arbitrary Isabelle theorems.
1263 It is the responsibility of the user to ensure that the external
1264 reasoner is as trustworthy as the application requires. Another
1265 typical source of errors is the linkup between Isabelle and the
1266 external tool, not just its concrete implementation, but also the
1267 required translation between two different logical environments.
1269 Isabelle merely guarantees well-formedness of the propositions being
1270 asserted, and records within the internal derivation object how
1271 presumed theorems depend on unproven suppositions.
1273 \begin{matharray}{rcl}
1274 \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1278 'oracle' name '=' text
1284 \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML
1285 expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
1286 ML function of type \verb|'a -> thm|, which is bound to the
1287 global identifier \verb|name|. This acts like an infinitary
1288 specification of axioms! Invoking the oracle only works within the
1289 scope of the resulting theory.
1293 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
1294 defining a new primitive rule as oracle, and turning it into a proof
1296 \end{isamarkuptext}%
1299 \isamarkupsection{Name spaces%
1303 \begin{isamarkuptext}%
1304 \begin{matharray}{rcl}
1305 \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1306 \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1307 \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1311 'hide' ('(open)')? name (nameref + )
1315 Isabelle organizes any kind of name declarations (of types,
1316 constants, theorems etc.) by separate hierarchically structured name
1317 spaces. Normally the user does not have to control the behavior of
1318 name spaces by hand, yet the following commands provide some way to
1323 \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
1324 name declaration mode. Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
1325 the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
1326 names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
1328 Note that global names are prone to get hidden accidently later,
1329 when qualified names of the same base name are introduced.
1331 \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
1332 declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
1333 \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
1334 (unqualified) names may never be hidden.
1336 Note that hiding name space accesses has no impact on logical
1337 declarations --- they remain valid internally. Entities that are no
1338 longer accessible to the user are printed with the special qualifier
1339 ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
1342 \end{isamarkuptext}%
1350 \isacommand{end}\isamarkupfalse%
1360 %%% Local Variables:
1362 %%% TeX-master: "root"