%
\begin{isabellebody}%
\def\isabellecontext{prelim}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Preliminaries%
}
\isamarkuptrue%
%
\isamarkupsection{Contexts \label{sec:context}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A logical context represents the background that is required for
formulating statements and composing proofs. It acts as a medium to
produce formal content, depending on earlier material (declarations,
results etc.).
For example, derivations within the Isabelle/Pure logic can be
described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
within the theory \isa{{\isasymTheta}}. There are logical reasons for
keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
liberal about supporting type constructors and schematic
polymorphism of constants and axioms, while the inner calculus of
\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with
fixed type variables in the assumptions).
\medskip Contexts and derivations are linked by the following key
principles:
\begin{itemize}
\item Transfer: monotonicity of derivations admits results to be
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}}.
\item Export: discharge of hypotheses admits results to be exported
into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
\isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here,
only the \isa{{\isasymGamma}} part is affected.
\end{itemize}
\medskip By modeling the main characteristics of the primitive
\isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any
particular logical content, we arrive at the fundamental notions of
\emph{theory context} and \emph{proof context} in Isabelle/Isar.
These implement a certain policy to manage arbitrary \emph{context
data}. There is a strongly-typed mechanism to declare new kinds of
data at compile time.
The internal bootstrap process of Isabelle/Pure eventually reaches a
stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!
Various additional data slots support all kinds of mechanisms that
are not necessarily part of the core logic.
For example, there would be data for canonical introduction and
elimination rules for arbitrary operators (depending on the
object-logic and application), which enables users to perform
standard proof steps implicitly (cf.\ the \isa{rule} method
\cite{isabelle-isar-ref}).
\medskip Thus Isabelle/Isar is able to bring forth more and more
concepts successively. In particular, an object-logic like
Isabelle/HOL continues the Isabelle/Pure setup by adding specific
components for automated reasoning (classical reasoner, tableau
prover, structured induction etc.) and derived specification
mechanisms (inductive predicates, recursive functions etc.). All of
this is ultimately based on the generic data management by theory
and proof contexts introduced here.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Theory context \label{sec:context-theory}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Theory}{FIXME}
A \emph{theory} is a data container with explicit named and unique
identifier. Theories are related by a (nominal) sub-theory
relation, which corresponds to the dependency graph of the original
construction; each theory is derived from a certain sub-graph of
ancestor theories.
The \isa{merge} operation produces the least upper bound of two
theories, which actually degenerates into absorption of one theory
into the other (due to the nominal sub-theory relation).
The \isa{begin} operation starts a new theory by importing
several parent theories and entering a special \isa{draft} mode,
which is sustained until the final \isa{end} operation. A draft
theory acts like a linear type, where updates invalidate earlier
versions. An invalidated draft is called ``stale''.
The \isa{checkpoint} operation produces an intermediate stepping
stone that will survive the next update: both the original and the
changed theory remain valid and are related by the sub-theory
relation. Checkpointing essentially recovers purely functional
theory values, at the expense of some extra internal bookkeeping.
The \isa{copy} operation produces an auxiliary version that has
the same data content, but is unrelated to the original: updates of
the copy do not affect the original, neither does the sub-theory
relation hold.
\medskip The example in \figref{fig:ex-theory} below shows a theory
graph derived from \isa{Pure}, with theory \isa{Length}
importing \isa{Nat} and \isa{List}. The body of \isa{Length} consists of a sequence of updates, working mostly on
drafts. Intermediate checkpoints may occur as well, due to the
history mechanism provided by the Isar top-level, cf.\
\secref{sec:isar-toplevel}.
\begin{figure}[htb]
\begin{center}
\begin{tabular}{rcccl}
& & \isa{Pure} \\
& & \isa{{\isasymdown}} \\
& & \isa{FOL} \\
& $\swarrow$ & & $\searrow$ & \\
$Nat$ & & & & \isa{List} \\
& $\searrow$ & & $\swarrow$ \\
& & \isa{Length} \\
& & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
& & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
& & $\vdots$~~ \\
& & \isa{{\isasymbullet}}~~ \\
& & $\vdots$~~ \\
& & \isa{{\isasymbullet}}~~ \\
& & $\vdots$~~ \\
& & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
\end{tabular}
\caption{A theory definition depending on ancestors}\label{fig:ex-theory}
\end{center}
\end{figure}
\medskip There is a separate notion of \emph{theory reference} for
maintaining a live link to an evolving theory context: updates on
drafts are propagated automatically. The dynamic stops after an
explicit \isa{end} only.
Derived entities may store a theory reference in order to indicate
the context they belong to. This implicitly assumes monotonic
reasoning, because the referenced context may become larger without
further notice.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{theory}\verb|type theory| \\
\indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
\indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
\indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
\indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
\indexmltype{theory-ref}\verb|type theory_ref| \\
\indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
\indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
\end{mldecls}
\begin{description}
\item \verb|theory| represents theory contexts. This is
essentially a linear type! Most operations destroy the original
version, which then becomes ``stale''.
\item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
compares theories according to the inherent graph structure of the
construction. This sub-theory relation is a nominal approximation
of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
\item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
absorbs one theory into the other. This fails for unrelated
theories!
\item \verb|Theory.checkpoint|~\isa{thy} produces a safe
stepping stone in the linear development of \isa{thy}. The next
update will result in two related, valid theories.
\item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The result is not
related to the original; the original is unchanched.
\item \verb|theory_ref| represents a sliding reference to an
always valid theory; updates on the original are propagated
automatically.
\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
evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Proof context \label{sec:context-proof}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Proof context}{The static context of a structured proof,
acts like a local ``theory'' of the current portion of Isar proof
text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a
generic notion of introducing and discharging hypotheses.
Arbritrary auxiliary context data may be adjoined.}
A proof context is a container for pure data with a back-reference
to the theory it belongs to. The \isa{init} operation creates a
proof context from a given theory. Modifications to draft theories
are propagated to the proof context as usual, but there is also an
explicit \isa{transfer} operation to force resynchronization
with more substantial updates to the underlying theory. The actual
context data does not require any special bookkeeping, thanks to the
lack of destructive features.
Entities derived in a proof context need to record inherent logical
requirements explicitly, since there is no separate context
identification as for theories. For example, hypotheses used in
primitive derivations (cf.\ \secref{sec:thms}) are recorded
separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
sure. Results could still leak into an alien proof context do to
programming errors, but Isabelle/Isar includes some extra validity
checks in critical positions, notably at the end of sub-proof.
Proof contexts may be manipulated arbitrarily, although the common
discipline is to follow block structure as a mental model: a given
context is extended consecutively, and results are exported back
into the original context. Note that the Isar proof states model
block-structured reasoning explicitly, using a stack of proof
contexts internally, cf.\ \secref{sec:isar-proof-state}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Proof.context}\verb|type Proof.context| \\
\indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
\indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
\indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
\end{mldecls}
\begin{description}
\item \verb|Proof.context| represents proof contexts. Elements
of this type are essentially pure values, with a sliding reference
to the background theory.
\item \verb|ProofContext.init|~\isa{thy} produces a proof context
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
background theory from \isa{ctxt}, dereferencing its internal
\verb|theory_ref|.
\item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
background theory of \isa{ctxt} to the super theory \isa{thy}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Generic contexts \label{sec:generic-context}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A generic context is the disjoint sum of either a theory or proof
context. Occasionally, this enables uniform treatment of generic
context data, typically extra-logical information. Operations on
generic contexts include the usual injections, partial selections,
and combinators for lifting operations on either component of the
disjoint sum.
Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
can always be selected from the sum, while a proof context might
have to be constructed by an ad-hoc \isa{init} operation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Context.generic}\verb|type Context.generic| \\
\indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
\indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
\end{mldecls}
\begin{description}
\item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
constructors \verb|Context.Theory| and \verb|Context.Proof|.
\item \verb|Context.theory_of|~\isa{context} always produces a
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
context data with each invocation).
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Context data \label{sec:context-data}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The main purpose of theory and proof contexts is to manage arbitrary
data. New data types can be declared incrementally at compile time.
There are separate declaration mechanisms for any of the three kinds
of contexts: theory, proof, generic.
\paragraph{Theory data} may refer to destructive entities, which are
maintained in direct correspondence to the linear evolution of
theory values, including explicit copies.\footnote{Most existing
instances of destructive theory data are merely historical relics
(e.g.\ the destructive theorem storage, and destructive hints for
the Simplifier and Classical rules).} A theory data declaration
needs to implement the following specification (depending on type
\isa{T}):
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
\isa{empty{\isacharcolon}\ T} & initial value \\
\isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
\isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
\isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
\isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
\end{tabular}
\medskip
\noindent The \isa{name} acts as a comment for diagnostic
messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both
should also include the functionality of \isa{copy} for impure
data.
\paragraph{Proof context data} is purely functional. A declaration
needs to implement the following specification:
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
\isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
\end{tabular}
\medskip
\noindent The \isa{init} operation is supposed to produce a pure
value from the given background theory. The remainder is analogous
to theory data.
\paragraph{Generic data} provides a hybrid interface for both theory
and proof data. The declaration is essentially the same as for
(pure) theory data, without \isa{copy}, though. The \isa{init} operation for proof contexts merely selects the current data
value from the background theory.
\bigskip In any case, a data declaration of type \isa{T} results
in the following interface:
\medskip
\begin{tabular}{ll}
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
\isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
\isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
\isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
\isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit}
\end{tabular}
\medskip
\noindent Here \isa{init} needs to be applied to the current
theory context once, in order to register the initial setup. The
other operations provide access for the particular kind of context
(theory, proof, or generic context). Note that this is a safe
interface: there is no other way to access the corresponding data
slot of a context. By keeping these operations private, a component
may maintain abstract values authentically, without other components
interfering.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
\indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
\indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
\end{mldecls}
\begin{description}
\item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
type \verb|theory| according to the specification provided as
argument structure. The resulting structure provides data init and
access operations as described above.
\item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
\verb|TheoryDataFun| for type \verb|Proof.context|.
\item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
\verb|TheoryDataFun| for type \verb|Context.generic|.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsection{Names%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
In principle, a name is just a string, but there are various
convention for encoding additional structure.
For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
qualified name. The most basic constituents of names may have their
own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Strings of symbols%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
plain ASCII characters as well as an infinite collection of named
symbols (for greek, math etc.).}
A \emph{symbol} constitutes the smallest textual unit in Isabelle
--- raw characters are normally not encountered. Isabelle strings
consist of a sequence of symbols, represented as a packed string or
a list of symbols. Each symbol is in itself a small string, which
is of one of the following forms:
\begin{enumerate}
\item singleton ASCII character ``\isa{c}'' (character code
0--127), for example ``\verb,a,'',
\item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
\item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<^bold>,'',
\item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
\isa{text} is constists of printable characters excluding
``\verb,.,'' and ``\verb,>,'', for example
``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
\item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
``\verb,\,\verb,<^raw42>,''.
\end{enumerate}
\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
regular symbols and control symbols, but a fixed collection of
standard symbols is treated specifically. For example,
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
which means it may occur within regular Isabelle identifier syntax.
Note that the character set underlying Isabelle symbols is plain
7-bit ASCII. Since 8-bit characters are passed through
transparently, Isabelle may process Unicode/UCS data (in UTF-8
encoding) as well. Unicode provides its own collection of
mathematical symbols, but there is no built-in link to the ones of
Isabelle.
\medskip Output of Isabelle symbols depends on the print mode
(\secref{FIXME}). For example, the standard {\LaTeX} setup of the
Isabelle document preparation system would present
``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
\indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
\indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
\indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
\indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
\indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
\indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
\indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
\end{mldecls}
\begin{description}
\item \verb|Symbol.symbol| represents Isabelle symbols. This
type is an alias for \verb|string|, but emphasizes the
specific format encountered here.
\item \verb|Symbol.explode|~\isa{str} produces a symbol list
from the packed form that. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
Isabelle!
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
symbols according to fixed syntactic conventions of Isabelle, cf.\
\cite{isabelle-isar-ref}.
\item \verb|Symbol.sym| is a concrete datatype that represents
the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
symbol into the datatype version.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Basic names \label{sec:basic-names}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \emph{basic name} essentially consists of a single Isabelle
identifier. There are conventions to mark separate classes of basic
names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
underscore means \emph{internal name}, two underscores means
\emph{Skolem name}, three underscores means \emph{internal Skolem
name}.
For example, the basic name \isa{foo} has the internal version
\isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
Such special versions are required for bookkeeping of names that are
apart from anything that may appear in the text given by the user.
In particular, system generated variables in high-level Isar proof
contexts are usually marked as internal, which prevents mysterious
name references such as \isa{xaa} in the text.
\medskip Basic manipulations of binding scopes requires names to be
modified. A \emph{name context} contains a collection of already
used names, which is maintained by the \isa{declare} operation.
The \isa{invents} operation derives a number of fresh names
derived from a given starting point. For example, three names
derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
provided there are no clashes with already used names.
The \isa{variants} operation produces fresh names by
incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}). For example, name \isa{foo} results in variants
\isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
unused variant from this list.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{Name.internal}\verb|Name.internal: string -> string| \\
\indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
\indexmltype{Name.context}\verb|type Name.context| \\
\indexml{Name.context}\verb|Name.context: Name.context| \\
\indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
\indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
\indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
\end{mldecls}
\begin{description}
\item \verb|Name.internal|~\isa{name} produces an internal name
by adding one underscore.
\item \verb|Name.skolem|~\isa{name} produces a Skolem name by
adding two underscores.
\item \verb|Name.context| represents the context of already used
names; the initial value is \verb|Name.context|.
\item \verb|Name.declare|~\isa{name} declares \isa{name} as
being used.
\item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Indexed names%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
name with a natural number. This representation allows efficient
renaming by incrementing the second component only. To rename two
collections of indexnames apart from each other, first determine the
maximum index \isa{maxidx} of the first collection, then
increment all indexes of the second collection by \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}. Note that the maximum index of an empty collection is \isa{{\isacharminus}{\isadigit{1}}}.
Isabelle syntax observes the following rules for representing an
indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
\begin{itemize}
\item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
\item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
\item \isa{{\isacharquery}x{\isachardot}i} else.
\end{itemize}
Occasionally, basic names and indexed names are injected into the
same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
to encode basic names.
\medskip Indexnames may acquire arbitrary large index numbers over
time. Results are usually normalized towards \isa{{\isadigit{0}}} at certain
checkpoints, such that the very end of a proof. This works by
producing variants of the corresponding basic names
(\secref{sec:basic-names}). For example, the collection \isa{{\isacharquery}x{\isachardot}{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{4}}{\isadigit{2}}} then becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{indexname}\verb|type indexname| \\
\end{mldecls}
\begin{description}
\item \verb|indexname| represents indexed names. This is an
abbreviation for \verb|string * int|. The second component is
usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
is used to embed plain names.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Qualified names and name spaces%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \emph{qualified name} consists of a non-empty sequence of basic
name components. The packed representation a dot as separator, for
example in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called
\emph{base} name, the remaining prefix \emph{qualifier} (which may
be empty).
The empty name is commonly used as an indication of unnamed
entities, if this makes any sense. The operations on qualified
names are smart enough to pass through such improper names
unchanged.
The basic idea of qualified names is to encode a hierarchically
structured name spaces by recording the access path as part of the
name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
entity \isa{c} within a local structure \isa{b} of the
enclosing structure \isa{A}. Typically, name space hierarchies
consist of 1--3 levels, but this need not be always so.
\medskip A \isa{naming} policy tells how to turn a name
specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
externally.
For example, the default naming prefixes an implicit path from the
context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
partial \isa{path} specifications.
Normally, the naming is implicit in the theory or proof context.
There are separate versions of the corresponding operations for these
context types.
\medskip A \isa{name\ space} manages a collection of fully
internalized names, together with a mapping between external names
and internal names (in both directions). The corresponding \isa{intern} and \isa{extern} operations are mostly used for
parsing and printing only! The \isa{declare} operation augments
a name space according to a given naming policy.
By general convention, there are separate name spaces for each kind
of formal entity, such as logical constant, type, type class,
theorem etc. It is usually clear from the occurrence in concrete
syntax (or from the scope) which kind of entity a name refers to.
For example, the very same name \isa{c} may be used uniformly
for a constant, type, type class, which are from separate syntactic
categories. There is a common convention to name theorems
systematically, according to the name of the main logical entity
being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
theorems related to constant \isa{c}.
This technique of mapping names from one space into another requires
some care in order to avoid conflicts. In particular, theorem names
derived from type or class names are better suffixed in addition to
the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
\isa{c}, respectively.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
\indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
\indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
\indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
\indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
\indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
\indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
\indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
\indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
\indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
\indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
\indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
\indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
\indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
\indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
\end{mldecls}
\begin{description}
\item \verb|NameSpace.base|~\isa{name} returns the base name of a
qualified name.
\item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
of a qualified name.
\item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
appends two qualified names.
\item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
string representation and explicit list form of qualified names.
\item \verb|NameSpace.naming| represents the abstract concept of
a naming policy.
\item \verb|NameSpace.default_naming| is the default naming policy.
In a theory context, this is usually augmented by a path prefix
consisting of the theory name.
\item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
naming policy by extending its path.
\item \verb|NameSpace.full|\isa{naming\ name} turns a name
specification (usually a basic name) into the fully qualified
internal version, according to the given naming policy.
\item \verb|NameSpace.T| represents name spaces.
\item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
building name spaces in accordance to the usual theory data
management (\secref{sec:context-data}).
\item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
fully qualified name into the name space, with partial accesses
being derived from the given policy.
\item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
(partially qualified) external name.
This operation is mostly for parsing. Note that fully qualified
names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
\item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
(fully qualified) internal name.
This operation is mostly for printing. Note unqualified names are
produced via \verb|NameSpace.base|.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: