3 \def\isabellecontext{prelim}%
13 \isacommand{theory}\isamarkupfalse%
14 \ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
22 \isamarkupchapter{Preliminaries%
26 \isamarkupsection{Contexts \label{sec:context}%
30 \begin{isamarkuptext}%
31 A logical context represents the background that is required for
32 formulating statements and composing proofs. It acts as a medium to
33 produce formal content, depending on earlier material (declarations,
36 For example, derivations within the Isabelle/Pure logic can be
37 described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
38 proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
39 within the theory \isa{{\isasymTheta}}. There are logical reasons for
40 keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
41 liberal about supporting type constructors and schematic
42 polymorphism of constants and axioms, while the inner calculus of
43 \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with
44 fixed type variables in the assumptions).
46 \medskip Contexts and derivations are linked by the following key
51 \item Transfer: monotonicity of derivations admits results to be
52 transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
54 \item Export: discharge of hypotheses admits results to be exported
55 into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
56 implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
57 \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here,
58 only the \isa{{\isasymGamma}} part is affected.
62 \medskip By modeling the main characteristics of the primitive
63 \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any
64 particular logical content, we arrive at the fundamental notions of
65 \emph{theory context} and \emph{proof context} in Isabelle/Isar.
66 These implement a certain policy to manage arbitrary \emph{context
67 data}. There is a strongly-typed mechanism to declare new kinds of
70 The internal bootstrap process of Isabelle/Pure eventually reaches a
71 stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!
72 Various additional data slots support all kinds of mechanisms that
73 are not necessarily part of the core logic.
75 For example, there would be data for canonical introduction and
76 elimination rules for arbitrary operators (depending on the
77 object-logic and application), which enables users to perform
78 standard proof steps implicitly (cf.\ the \isa{rule} method
79 \cite{isabelle-isar-ref}).
81 \medskip Thus Isabelle/Isar is able to bring forth more and more
82 concepts successively. In particular, an object-logic like
83 Isabelle/HOL continues the Isabelle/Pure setup by adding specific
84 components for automated reasoning (classical reasoner, tableau
85 prover, structured induction etc.) and derived specification
86 mechanisms (inductive predicates, recursive functions etc.). All of
87 this is ultimately based on the generic data management by theory
88 and proof contexts introduced here.%
92 \isamarkupsubsection{Theory context \label{sec:context-theory}%
96 \begin{isamarkuptext}%
97 \glossary{Theory}{FIXME}
99 A \emph{theory} is a data container with explicit named and unique
100 identifier. Theories are related by a (nominal) sub-theory
101 relation, which corresponds to the dependency graph of the original
102 construction; each theory is derived from a certain sub-graph of
105 The \isa{merge} operation produces the least upper bound of two
106 theories, which actually degenerates into absorption of one theory
107 into the other (due to the nominal sub-theory relation).
109 The \isa{begin} operation starts a new theory by importing
110 several parent theories and entering a special \isa{draft} mode,
111 which is sustained until the final \isa{end} operation. A draft
112 theory acts like a linear type, where updates invalidate earlier
113 versions. An invalidated draft is called ``stale''.
115 The \isa{checkpoint} operation produces an intermediate stepping
116 stone that will survive the next update: both the original and the
117 changed theory remain valid and are related by the sub-theory
118 relation. Checkpointing essentially recovers purely functional
119 theory values, at the expense of some extra internal bookkeeping.
121 The \isa{copy} operation produces an auxiliary version that has
122 the same data content, but is unrelated to the original: updates of
123 the copy do not affect the original, neither does the sub-theory
126 \medskip The example in \figref{fig:ex-theory} below shows a theory
127 graph derived from \isa{Pure}, with theory \isa{Length}
128 importing \isa{Nat} and \isa{List}. The body of \isa{Length} consists of a sequence of updates, working mostly on
129 drafts. Intermediate checkpoints may occur as well, due to the
130 history mechanism provided by the Isar top-level, cf.\
131 \secref{sec:isar-toplevel}.
135 \begin{tabular}{rcccl}
137 & & \isa{{\isasymdown}} \\
139 & $\swarrow$ & & $\searrow$ & \\
140 \isa{Nat} & & & & \isa{List} \\
141 & $\searrow$ & & $\swarrow$ \\
143 & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
144 & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
146 & & \isa{{\isasymbullet}}~~ \\
148 & & \isa{{\isasymbullet}}~~ \\
150 & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
152 \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
156 \medskip There is a separate notion of \emph{theory reference} for
157 maintaining a live link to an evolving theory context: updates on
158 drafts are propagated automatically. Dynamic updating stops after
159 an explicit \isa{end} only.
161 Derived entities may store a theory reference in order to indicate
162 the context they belong to. This implicitly assumes monotonic
163 reasoning, because the referenced context may become larger without
174 \begin{isamarkuptext}%
176 \indexmltype{theory}\verb|type theory| \\
177 \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
178 \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
179 \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
180 \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
183 \indexmltype{theory-ref}\verb|type theory_ref| \\
184 \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
185 \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
190 \item \verb|theory| represents theory contexts. This is
191 essentially a linear type! Most operations destroy the original
192 version, which then becomes ``stale''.
194 \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
195 compares theories according to the inherent graph structure of the
196 construction. This sub-theory relation is a nominal approximation
197 of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
199 \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
200 absorbs one theory into the other. This fails for unrelated
203 \item \verb|Theory.checkpoint|~\isa{thy} produces a safe
204 stepping stone in the linear development of \isa{thy}. The next
205 update will result in two related, valid theories.
207 \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The result is not
208 related to the original; the original is unchanched.
210 \item \verb|theory_ref| represents a sliding reference to an
211 always valid theory; updates on the original are propagated
214 \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|. As the referenced theory
215 evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
228 \isamarkupsubsection{Proof context \label{sec:context-proof}%
232 \begin{isamarkuptext}%
233 \glossary{Proof context}{The static context of a structured proof,
234 acts like a local ``theory'' of the current portion of Isar proof
235 text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
236 judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a
237 generic notion of introducing and discharging hypotheses.
238 Arbritrary auxiliary context data may be adjoined.}
240 A proof context is a container for pure data with a back-reference
241 to the theory it belongs to. The \isa{init} operation creates a
242 proof context from a given theory. Modifications to draft theories
243 are propagated to the proof context as usual, but there is also an
244 explicit \isa{transfer} operation to force resynchronization
245 with more substantial updates to the underlying theory. The actual
246 context data does not require any special bookkeeping, thanks to the
247 lack of destructive features.
249 Entities derived in a proof context need to record inherent logical
250 requirements explicitly, since there is no separate context
251 identification as for theories. For example, hypotheses used in
252 primitive derivations (cf.\ \secref{sec:thms}) are recorded
253 separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
254 sure. Results could still leak into an alien proof context do to
255 programming errors, but Isabelle/Isar includes some extra validity
256 checks in critical positions, notably at the end of sub-proof.
258 Proof contexts may be manipulated arbitrarily, although the common
259 discipline is to follow block structure as a mental model: a given
260 context is extended consecutively, and results are exported back
261 into the original context. Note that the Isar proof states model
262 block-structured reasoning explicitly, using a stack of proof
263 contexts internally, cf.\ \secref{sec:isar-proof-state}.%
273 \begin{isamarkuptext}%
275 \indexmltype{Proof.context}\verb|type Proof.context| \\
276 \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
277 \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
278 \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
283 \item \verb|Proof.context| represents proof contexts. Elements
284 of this type are essentially pure values, with a sliding reference
285 to the background theory.
287 \item \verb|ProofContext.init|~\isa{thy} produces a proof context
288 derived from \isa{thy}, initializing all data.
290 \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
291 background theory from \isa{ctxt}, dereferencing its internal
294 \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
295 background theory of \isa{ctxt} to the super theory \isa{thy}.
308 \isamarkupsubsection{Generic contexts \label{sec:generic-context}%
312 \begin{isamarkuptext}%
313 A generic context is the disjoint sum of either a theory or proof
314 context. Occasionally, this enables uniform treatment of generic
315 context data, typically extra-logical information. Operations on
316 generic contexts include the usual injections, partial selections,
317 and combinators for lifting operations on either component of the
320 Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
321 can always be selected from the sum, while a proof context might
322 have to be constructed by an ad-hoc \isa{init} operation.%
332 \begin{isamarkuptext}%
334 \indexmltype{Context.generic}\verb|type Context.generic| \\
335 \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
336 \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
341 \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
342 constructors \verb|Context.Theory| and \verb|Context.Proof|.
344 \item \verb|Context.theory_of|~\isa{context} always produces a
345 theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
347 \item \verb|Context.proof_of|~\isa{context} always produces a
348 proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
349 context data with each invocation).
362 \isamarkupsubsection{Context data \label{sec:context-data}%
366 \begin{isamarkuptext}%
367 The main purpose of theory and proof contexts is to manage arbitrary
368 data. New data types can be declared incrementally at compile time.
369 There are separate declaration mechanisms for any of the three kinds
370 of contexts: theory, proof, generic.
372 \paragraph{Theory data} may refer to destructive entities, which are
373 maintained in direct correspondence to the linear evolution of
374 theory values, including explicit copies.\footnote{Most existing
375 instances of destructive theory data are merely historical relics
376 (e.g.\ the destructive theorem storage, and destructive hints for
377 the Simplifier and Classical rules).} A theory data declaration
378 needs to implement the following specification (depending on type
383 \isa{name{\isacharcolon}\ string} \\
384 \isa{empty{\isacharcolon}\ T} & initial value \\
385 \isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
386 \isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
387 \isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
388 \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
392 \noindent The \isa{name} acts as a comment for diagnostic
393 messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both
394 should also include the functionality of \isa{copy} for impure
397 \paragraph{Proof context data} is purely functional. A declaration
398 needs to implement the following specification:
402 \isa{name{\isacharcolon}\ string} \\
403 \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
404 \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
408 \noindent The \isa{init} operation is supposed to produce a pure
409 value from the given background theory. The remainder is analogous
412 \paragraph{Generic data} provides a hybrid interface for both theory
413 and proof data. The declaration is essentially the same as for
414 (pure) theory data, without \isa{copy}, though. The \isa{init} operation for proof contexts merely selects the current data
415 value from the background theory.
417 \bigskip In any case, a data declaration of type \isa{T} results
418 in the following interface:
422 \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
423 \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
424 \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
425 \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
426 \isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit}
430 \noindent Here \isa{init} needs to be applied to the current
431 theory context once, in order to register the initial setup. The
432 other operations provide access for the particular kind of context
433 (theory, proof, or generic context). Note that this is a safe
434 interface: there is no other way to access the corresponding data
435 slot of a context. By keeping these operations private, a component
436 may maintain abstract values authentically, without other components
447 \begin{isamarkuptext}%
449 \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
450 \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
451 \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
456 \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
457 type \verb|theory| according to the specification provided as
458 argument structure. The resulting structure provides data init and
459 access operations as described above.
461 \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
462 \verb|TheoryDataFun| for type \verb|Proof.context|.
464 \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
465 \verb|TheoryDataFun| for type \verb|Context.generic|.
478 \isamarkupsection{Names%
482 \begin{isamarkuptext}%
483 In principle, a name is just a string, but there are various
484 convention for encoding additional structure. For example, ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a qualified name consisting of
485 three basic name components. The individual constituents of a name
486 may have further substructure, e.g.\ the string
487 ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.%
491 \isamarkupsubsection{Strings of symbols%
495 \begin{isamarkuptext}%
496 \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
497 plain ASCII characters as well as an infinite collection of named
498 symbols (for greek, math etc.).}
500 A \emph{symbol} constitutes the smallest textual unit in Isabelle
501 --- raw characters are normally not encountered at all. Isabelle
502 strings consist of a sequence of symbols, represented as a packed
503 string or a list of strings. Each symbol is in itself a small
504 string, which has either one of the following forms:
508 \item a single ASCII character ``\isa{c}'', for example
511 \item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
512 for example ``\verb,\,\verb,<alpha>,'',
514 \item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
515 for example ``\verb,\,\verb,<^bold>,'',
517 \item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''
518 where \isa{text} constists of printable characters excluding
519 ``\verb,.,'' and ``\verb,>,'', for example
520 ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
522 \item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
523 ``\verb,\,\verb,<^raw42>,''.
527 \noindent The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many
528 regular symbols and control symbols, but a fixed collection of
529 standard symbols is treated specifically. For example,
530 ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
531 may occur within regular Isabelle identifiers.
533 Since the character set underlying Isabelle symbols is 7-bit ASCII
534 and 8-bit characters are passed through transparently, Isabelle may
535 also process Unicode/UCS data in UTF-8 encoding. Unicode provides
536 its own collection of mathematical symbols, but there is no built-in
537 link to the standard collection of Isabelle.
539 \medskip Output of Isabelle symbols depends on the print mode
540 (\secref{FIXME}). For example, the standard {\LaTeX} setup of the
541 Isabelle document preparation system would present
542 ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
543 ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
553 \begin{isamarkuptext}%
555 \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
556 \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
557 \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
558 \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
559 \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
560 \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
563 \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
564 \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
569 \item \verb|Symbol.symbol| represents individual Isabelle
570 symbols; this is an alias for \verb|string|.
572 \item \verb|Symbol.explode|~\isa{str} produces a symbol list
573 from the packed form. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
576 \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
577 symbols according to fixed syntactic conventions of Isabelle, cf.\
578 \cite{isabelle-isar-ref}.
580 \item \verb|Symbol.sym| is a concrete datatype that represents
581 the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
583 \item \verb|Symbol.decode| converts the string representation of a
584 symbol into the datatype version.
597 \isamarkupsubsection{Basic names \label{sec:basic-names}%
601 \begin{isamarkuptext}%
602 A \emph{basic name} essentially consists of a single Isabelle
603 identifier. There are conventions to mark separate classes of basic
604 names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
605 underscore means \emph{internal name}, two underscores means
606 \emph{Skolem name}, three underscores means \emph{internal Skolem
609 For example, the basic name \isa{foo} has the internal version
610 \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
612 These special versions provide copies of the basic name space, apart
613 from anything that normally appears in the user text. For example,
614 system generated variables in Isar proof contexts are usually marked
615 as internal, which prevents mysterious name references like \isa{xaa} to appear in the text.
617 \medskip Manipulating binding scopes often requires on-the-fly
618 renamings. A \emph{name context} contains a collection of already
619 used names. The \isa{declare} operation adds names to the
622 The \isa{invents} operation derives a number of fresh names from
623 a given starting point. For example, the first three names derived
624 from \isa{a} are \isa{a}, \isa{b}, \isa{c}.
626 The \isa{variants} operation produces fresh names by
627 incrementing tentative names as base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}) until all clashes are resolved. For example, name \isa{foo} results in variants \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab} etc.; each renaming
628 step picks the next unused variant from this sequence.%
638 \begin{isamarkuptext}%
640 \indexml{Name.internal}\verb|Name.internal: string -> string| \\
641 \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
644 \indexmltype{Name.context}\verb|type Name.context| \\
645 \indexml{Name.context}\verb|Name.context: Name.context| \\
646 \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
647 \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
648 \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
653 \item \verb|Name.internal|~\isa{name} produces an internal name
654 by adding one underscore.
656 \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
657 adding two underscores.
659 \item \verb|Name.context| represents the context of already used
660 names; the initial value is \verb|Name.context|.
662 \item \verb|Name.declare|~\isa{name} enters a used name into the
665 \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
667 \item \verb|Name.variants|~\isa{names\ context} produces fresh
668 varians of \isa{names}; the result is entered into the context.
681 \isamarkupsubsection{Indexed names%
685 \begin{isamarkuptext}%
686 An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
687 name and a natural number. This representation allows efficient
688 renaming by incrementing the second component only. The canonical
689 way to rename two collections of indexnames apart from each other is
690 this: determine the maximum index \isa{maxidx} of the first
691 collection, then increment all indexes of the second collection by
692 \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}; the maximum index of an empty collection is
693 \isa{{\isacharminus}{\isadigit{1}}}.
695 Occasionally, basic names and indexed names are injected into the
696 same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
697 to encode basic names.
699 \medskip Isabelle syntax observes the following rules for
700 representing an indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
704 \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}},
706 \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
708 \item \isa{{\isacharquery}x{\isachardot}i} otherwise.
712 Indexnames may acquire large index numbers over time. Results are
713 normalized towards \isa{{\isadigit{0}}} at certain checkpoints, notably at
714 the end of a proof. This works by producing variants of the
715 corresponding basic name components. For example, the collection
716 \isa{{\isacharquery}x{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isadigit{4}}{\isadigit{2}}} becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
726 \begin{isamarkuptext}%
728 \indexmltype{indexname}\verb|type indexname| \\
733 \item \verb|indexname| represents indexed names. This is an
734 abbreviation for \verb|string * int|. The second component is
735 usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
736 is used to embed basic names into this type.
749 \isamarkupsubsection{Qualified names and name spaces%
753 \begin{isamarkuptext}%
754 A \emph{qualified name} consists of a non-empty sequence of basic
755 name components. The packed representation uses a dot as separator,
756 as in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called \emph{base}
757 name, the remaining prefix \emph{qualifier} (which may be empty).
758 The idea of qualified names is to encode nested structures by
759 recording the access paths as qualifiers. For example, an item
760 named ``\isa{A{\isachardot}b{\isachardot}c}'' may be understood as a local entity \isa{c}, within a local structure \isa{b}, within a global
761 structure \isa{A}. Typically, name space hierarchies consist of
762 1--2 levels of qualification, but this need not be always so.
764 The empty name is commonly used as an indication of unnamed
765 entities, whenever this makes any sense. The basic operations on
766 qualified names are smart enough to pass through such improper names
769 \medskip A \isa{naming} policy tells how to turn a name
770 specification into a fully qualified internal name (by the \isa{full} operation), and how fully qualified names may be accessed
771 externally. For example, the default naming policy is to prefix an
772 implicit path: \isa{full\ x} produces \isa{path{\isachardot}x}, and the
773 standard accesses for \isa{path{\isachardot}x} include both \isa{x} and
774 \isa{path{\isachardot}x}. Normally, the naming is implicit in the theory or
775 proof context; there are separate versions of the corresponding.
777 \medskip A \isa{name\ space} manages a collection of fully
778 internalized names, together with a mapping between external names
779 and internal names (in both directions). The corresponding \isa{intern} and \isa{extern} operations are mostly used for
780 parsing and printing only! The \isa{declare} operation augments
781 a name space according to the accesses determined by the naming
784 \medskip As a general principle, there is a separate name space for
785 each kind of formal entity, e.g.\ logical constant, type
786 constructor, type class, theorem. It is usually clear from the
787 occurrence in concrete syntax (or from the scope) which kind of
788 entity a name refers to. For example, the very same name \isa{c} may be used uniformly for a constant, type constructor, and
791 There are common schemes to name theorems systematically, according
792 to the name of the main logical entity involved, e.g.\ \isa{c{\isachardot}intro} for a canonical theorem related to constant \isa{c}.
793 This technique of mapping names from one space into another requires
794 some care in order to avoid conflicts. In particular, theorem names
795 derived from a type constructor or type class are better suffixed in
796 addition to the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro}
797 and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c}
798 and class \isa{c}, respectively.%
808 \begin{isamarkuptext}%
810 \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
811 \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
812 \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
813 \indexml{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
814 \indexml{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
817 \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
818 \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
819 \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
820 \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
823 \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
824 \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
825 \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
826 \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
827 \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
828 \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
833 \item \verb|NameSpace.base|~\isa{name} returns the base name of a
836 \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
839 \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
840 appends two qualified names.
842 \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
843 representation and the explicit list form of qualified names.
845 \item \verb|NameSpace.naming| represents the abstract concept of
848 \item \verb|NameSpace.default_naming| is the default naming policy.
849 In a theory context, this is usually augmented by a path prefix
850 consisting of the theory name.
852 \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
853 naming policy by extending its path component.
855 \item \verb|NameSpace.full|\isa{naming\ name} turns a name
856 specification (usually a basic name) into the fully qualified
857 internal version, according to the given naming policy.
859 \item \verb|NameSpace.T| represents name spaces.
861 \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
862 maintaining name spaces according to theory data management
863 (\secref{sec:context-data}).
865 \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
866 fully qualified name into the name space, with external accesses
867 determined by the naming policy.
869 \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
870 (partially qualified) external name.
872 This operation is mostly for parsing! Note that fully qualified
873 names stemming from declarations are produced via \verb|NameSpace.full| (or its derivatives for \verb|theory| and
874 \verb|Proof.context|).
876 \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
877 (fully qualified) internal name.
879 This operation is mostly for printing! Note unqualified names are
880 produced via \verb|NameSpace.base|.
898 \isacommand{end}\isamarkupfalse%
910 %%% TeX-master: "root"