%

 \begin{isabellebody}%

 \def\isabellecontext{Prelim}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isatagtheory

 \isacommand{theory}\isamarkupfalse%

 \ Prelim\isanewline

 \isakeyword{imports}\ Base\isanewline

 \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{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}}, which means that a

   proposition \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} is derivable from hypotheses \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}

   within the theory \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}}.  There are logical reasons for

   keeping \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} separate: theories can be

   liberal about supporting type constructors and schematic

   polymorphism of constants and axioms, while the inner calculus of

   \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\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{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} implies \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} for contexts \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}.

   \item Export: discharge of hypotheses admits results to be exported

   into a \emph{smaller} context, i.e.\ \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}}

   implies \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C54686574613E}{\isasymTheta}}\ {\isaliteral{5C3C44656C74613E}{\isasymDelta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}} where \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} and

   \isa{{\isaliteral{5C3C44656C74613E}{\isasymDelta}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}.  Note that \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} remains unchanged here,

   only the \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} part is affected.

   \end{itemize}

   \medskip By modeling the main characteristics of the primitive

   \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\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{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} and \isa{{\isaliteral{5C3C47616D6D613E}{\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}%

 A \emph{theory} is a data container with explicit name 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.  To this end, the system maintains a set of

   symbolic ``identification stamps'' within each theory.

   In order to avoid the full-scale overhead of explicit sub-theory

   identification of arbitrary intermediate stages, a theory is

   switched into \isa{draft} mode under certain circumstances.  A

   draft theory acts like a linear type, where updates invalidate

   earlier versions.  An invalidated draft is called \emph{stale}.

   The \isa{checkpoint} operation produces a safe stepping stone

   that will survive the next update without becoming stale: both the

   old and the new 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.

   The \isa{merge} operation produces the least upper bound of two

   theories, which actually degenerates into absorption of one theory

   into the other (according to the nominal sub-theory relation).

   The \isa{begin} operation starts a new theory by importing

   several parent theories and entering a special mode of nameless

   incremental updates, until the final \isa{end} operation is

   performed.

   \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 internally, while transaction boundaries of Isar top-level

   commands (\secref{sec:isar-toplevel}) are guaranteed to be safe

   checkpoints.

   \begin{figure}[htb]

   \begin{center}

   \begin{tabular}{rcccl}

         &            & \isa{Pure} \\

         &            & \isa{{\isaliteral{5C3C646F776E3E}{\isasymdown}}} \\

         &            & \isa{FOL} \\

         & $\swarrow$ &              & $\searrow$ & \\

   \isa{Nat} &    &              &            & \isa{List} \\

         & $\searrow$ &              & $\swarrow$ \\

         &            & \isa{Length} \\

         &            & \multicolumn{3}{l}{~~\hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}} \\

         &            & \multicolumn{3}{l}{~~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}} \\

         &            & $\vdots$~~ \\

         &            & \isa{{\isaliteral{5C3C62756C6C65743E}{\isasymbullet}}}~~ \\

         &            & $\vdots$~~ \\

         &            & \isa{{\isaliteral{5C3C62756C6C65743E}{\isasymbullet}}}~~ \\

         &            & $\vdots$~~ \\

         &            & \multicolumn{3}{l}{~~\hyperlink{command.end}{\mbox{\isa{\isacommand{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.  Dynamic updating stops when

   the next \isa{checkpoint} is reached.

   Derived entities may store a theory reference in order to indicate

   the formal context from which they are derived.  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}

   \indexdef{}{ML type}{theory}\verb|type theory| \\

   \indexdef{}{ML}{Theory.eq\_thy}\verb|Theory.eq_thy: theory * theory -> bool| \\

   \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\

   \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\

   \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\

   \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\

   \indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\

   \indexdef{}{ML}{Theory.parents\_of}\verb|Theory.parents_of: theory -> theory list| \\

   \indexdef{}{ML}{Theory.ancestors\_of}\verb|Theory.ancestors_of: theory -> theory list| \\

   \end{mldecls}

   \begin{mldecls}

   \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\

   \indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\

   \indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\

   \end{mldecls}

   \begin{description}

   \item Type \verb|theory| represents theory contexts.  This is

   essentially a linear type, with explicit runtime checking.

   Primitive theory operations destroy the original version, which then

   becomes ``stale''.  This can be prevented by explicit checkpointing,

   which the system does at least at the boundary of toplevel command

   transactions \secref{sec:isar-toplevel}.

   \item \verb|Theory.eq_thy|~\isa{{\isaliteral{28}{\isacharparenleft}}thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} check strict

   identity of two theories.

   \item \verb|Theory.subthy|~\isa{{\isaliteral{28}{\isacharparenleft}}thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} compares theories

   according to the intrinsic graph structure of the construction.

   This sub-theory relation is a nominal approximation of inclusion

   (\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}) of the corresponding content (according to the

   semantics of the ML modules that implement the data).

   \item \verb|Theory.checkpoint|~\isa{thy} produces a safe

   stepping stone in the linear development of \isa{thy}.  This

   changes the old theory, but the next update will result in two

   related, valid theories.

   \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data.  The copy is not related to the original,

   but the original is unchanged.

   \item \verb|Theory.merge|~\isa{{\isaliteral{28}{\isacharparenleft}}thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} absorbs one theory

   into the other, without changing \isa{thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} or \isa{thy\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.

   This version of ad-hoc theory merge fails for unrelated theories!

   \item \verb|Theory.begin_theory|~\isa{name\ parents} constructs

   a new theory based on the given parents.  This ML function is

   normally not invoked directly.

   \item \verb|Theory.parents_of|~\isa{thy} returns the direct

   ancestors of \isa{thy}.

   \item \verb|Theory.ancestors_of|~\isa{thy} returns all

   ancestors of \isa{thy} (not including \isa{thy} itself).

   \item Type \verb|theory_ref| represents a sliding reference to

   an always valid theory; updates on the original are propagated

   automatically.

   \item \verb|Theory.deref|~\isa{thy{\isaliteral{5F}{\isacharunderscore}}ref} turns a \verb|theory_ref| into an \verb|theory| value.  As the referenced

   theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.

   \item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isadelimmlantiq

 %

 \endisadelimmlantiq

 %

 \isatagmlantiq

 %

 \begin{isamarkuptext}%

 \begin{matharray}{rcl}

   \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   \end{matharray}

   \begin{railoutput}

 \rail@begin{2}{}

 \rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[]

 \rail@bar

 \rail@nextbar{1}

 \rail@nont{\isa{nameref}}[]

 \rail@endbar

 \rail@end

 \end{railoutput}

   \begin{description}

   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}theory{\isaliteral{7D}{\isacharbraceright}}} refers to the background theory of the

   current context --- as abstract value.

   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}theory\ A{\isaliteral{7D}{\isacharbraceright}}} refers to an explicitly named ancestor

   theory \isa{A} of the background theory of the current context

   --- as abstract value.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlantiq

 {\isafoldmlantiq}%

 %

 \isadelimmlantiq

 %

 \endisadelimmlantiq

 %

 \isamarkupsubsection{Proof context \label{sec:context-proof}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 A proof context is a container for pure data with a

   back-reference to the theory from which it is derived.  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.

   Entities derived in a proof context need to record logical

   requirements explicitly, since there is no separate context

   identification or symbolic inclusion as for theories.  For example,

   hypotheses used in primitive derivations (cf.\ \secref{sec:thms})

   are recorded separately within the sequent \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}}, just to

   make double sure.  Results could still leak into an alien proof

   context due to programming errors, but Isabelle/Isar includes some

   extra validity checks in critical positions, notably at the end of a

   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 an Isar proof state models

   block-structured reasoning explicitly, using a stack of proof

   contexts internally.  For various technical reasons, the background

   theory of an Isar proof state must not be changed while the proof is

   still under construction!%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\

   \indexdef{}{ML}{Proof\_Context.init\_global}\verb|Proof_Context.init_global: theory -> Proof.context| \\

   \indexdef{}{ML}{Proof\_Context.theory\_of}\verb|Proof_Context.theory_of: Proof.context -> theory| \\

   \indexdef{}{ML}{Proof\_Context.transfer}\verb|Proof_Context.transfer: theory -> Proof.context -> Proof.context| \\

   \end{mldecls}

   \begin{description}

   \item Type \verb|Proof.context| represents proof contexts.

   Elements of this type are essentially pure values, with a sliding

   reference to the background theory.

   \item \verb|Proof_Context.init_global|~\isa{thy} produces a proof context

   derived from \isa{thy}, initializing all data.

   \item \verb|Proof_Context.theory_of|~\isa{ctxt} selects the

   background theory from \isa{ctxt}, dereferencing its internal

   \verb|theory_ref|.

   \item \verb|Proof_Context.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

 %

 \isadelimmlantiq

 %

 \endisadelimmlantiq

 %

 \isatagmlantiq

 %

 \begin{isamarkuptext}%

 \begin{matharray}{rcl}

   \indexdef{}{ML antiquotation}{context}\hypertarget{ML antiquotation.context}{\hyperlink{ML antiquotation.context}{\mbox{\isa{context}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   \end{matharray}

   \begin{description}

   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}context{\isaliteral{7D}{\isacharbraceright}}} refers to \emph{the} context at

   compile-time --- as abstract value.  Independently of (local) theory

   or proof mode, this always produces a meaningful result.

   This is probably the most common antiquotation in interactive

   experimentation with ML inside Isar.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlantiq

 {\isafoldmlantiq}%

 %

 \isadelimmlantiq

 %

 \endisadelimmlantiq

 %

 \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{\isaliteral{5F}{\isacharunderscore}}of} and \isa{proof{\isaliteral{5F}{\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, which

   incurs a small runtime overhead.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\

   \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\

   \indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\

   \end{mldecls}

   \begin{description}

   \item Type \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|Proof_Context.theory_of| as required.

   \item \verb|Context.proof_of|~\isa{context} always produces a

   proof context from the generic \isa{context}, using \verb|Proof_Context.init_global| 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 (pure) 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} declarations need to implement the following

   SML signature:

   \medskip

   \begin{tabular}{ll}

   \isa{{\isaliteral{5C3C747970653E}{\isasymtype}}\ T} & representing type \\

   \isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ empty{\isaliteral{3A}{\isacharcolon}}\ T} & empty default value \\

   \isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ extend{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & re-initialize on import \\

   \isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ merge{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & join on import \\

   \end{tabular}

   \medskip

   The \isa{empty} value acts as initial default for \emph{any}

   theory that does not declare actual data content; \isa{extend}

   is acts like a unitary version of \isa{merge}.

   Implementing \isa{merge} can be tricky.  The general idea is

   that \isa{merge\ {\isaliteral{28}{\isacharparenleft}}data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} inserts those parts of \isa{data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} into \isa{data\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} that are not yet present, while

   keeping the general order of things.  The \verb|Library.merge|

   function on plain lists may serve as canonical template.

   Particularly note that shared parts of the data must not be

   duplicated by naive concatenation, or a theory graph that is like a

   chain of diamonds would cause an exponential blowup!

   \paragraph{Proof context data} declarations need to implement the

   following SML signature:

   \medskip

   \begin{tabular}{ll}

   \isa{{\isaliteral{5C3C747970653E}{\isasymtype}}\ T} & representing type \\

   \isa{{\isaliteral{5C3C76616C3E}{\isasymval}}\ init{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} & produce initial value \\

   \end{tabular}

   \medskip

   The \isa{init} operation is supposed to produce a pure value

   from the given background theory and should be somehow

   ``immediate''.  Whenever a proof context is initialized, which

   happens frequently, the the system invokes the \isa{init}

   operation of \emph{all} theory data slots ever declared.  This also

   means that one needs to be economic about the total number of proof

   data declarations in the system, i.e.\ each ML module should declare

   at most one, sometimes two data slots for its internal use.

   Repeated data declarations to simulate a record type should be

   avoided!

   \paragraph{Generic data} provides a hybrid interface for both theory

   and proof data.  The \isa{init} operation for proof contexts is

   predefined to select the current data value from the background

   theory.

   \bigskip Any of the above data declarations over type \isa{T}

   result in an ML structure with the following signature:

   \medskip

   \begin{tabular}{ll}

   \isa{get{\isaliteral{3A}{\isacharcolon}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} \\

   \isa{put{\isaliteral{3A}{\isacharcolon}}\ T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} \\

   \isa{map{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} \\

   \end{tabular}

   \medskip

   These other operations provide exclusive access for the particular

   kind of context (theory, proof, or generic context).  This interface

   observes the ML discipline for types and scopes: there is no other

   way to access the corresponding data slot of a context.  By keeping

   these operations private, an Isabelle/ML module may maintain

   abstract values authentically.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML functor}{Theory\_Data}\verb|functor Theory_Data| \\

   \indexdef{}{ML functor}{Proof\_Data}\verb|functor Proof_Data| \\

   \indexdef{}{ML functor}{Generic\_Data}\verb|functor Generic_Data| \\

   \end{mldecls}

   \begin{description}

   \item \verb|Theory_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\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|Proof_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\isacharparenright}}} is analogous to

   \verb|Theory_Data| for type \verb|Proof.context|.

   \item \verb|Generic_Data|\isa{{\isaliteral{28}{\isacharparenleft}}spec{\isaliteral{29}{\isacharparenright}}} is analogous to

   \verb|Theory_Data| for type \verb|Context.generic|.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isatagmlex

 %

 \begin{isamarkuptext}%

 The following artificial example demonstrates theory

   data: we maintain a set of terms that are supposed to be wellformed

   wrt.\ the enclosing theory.  The public interface is as follows:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlex

 {\isafoldmlex}%

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ signature\ WELLFORMED{\isaliteral{5F}{\isacharunderscore}}TERMS\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ sig\isanewline

 \ \ \ \ val\ get{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ term\ list\isanewline

 \ \ \ \ val\ add{\isaliteral{3A}{\isacharcolon}}\ term\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ theory\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ theory\isanewline

 \ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \begin{isamarkuptext}%

 The implementation uses private theory data internally, and

   only exposes an operation that involves explicit argument checking

   wrt.\ the given theory.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ structure\ Wellformed{\isaliteral{5F}{\isacharunderscore}}Terms{\isaliteral{3A}{\isacharcolon}}\ WELLFORMED{\isaliteral{5F}{\isacharunderscore}}TERMS\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ struct\isanewline

 \isanewline

 \ \ structure\ Terms\ {\isaliteral{3D}{\isacharequal}}\ Theory{\isaliteral{5F}{\isacharunderscore}}Data\isanewline

 \ \ {\isaliteral{28}{\isacharparenleft}}\isanewline

 \ \ \ \ type\ T\ {\isaliteral{3D}{\isacharequal}}\ term\ Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}T{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ \ \ val\ empty\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ \ \ val\ extend\ {\isaliteral{3D}{\isacharequal}}\ I{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ \ \ fun\ merge\ {\isaliteral{28}{\isacharparenleft}}ts{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ ts{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ \ \ \ \ Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}union\ Term{\isaliteral{5F}{\isacharunderscore}}Ord{\isaliteral{2E}{\isachardot}}fast{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \isanewline

 \ \ val\ get\ {\isaliteral{3D}{\isacharequal}}\ Terms{\isaliteral{2E}{\isachardot}}get{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \isanewline

 \ \ fun\ add\ raw{\isaliteral{5F}{\isacharunderscore}}t\ thy\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ \ \ let\isanewline

 \ \ \ \ \ \ val\ t\ {\isaliteral{3D}{\isacharequal}}\ Sign{\isaliteral{2E}{\isachardot}}cert{\isaliteral{5F}{\isacharunderscore}}term\ thy\ raw{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ \ \ in\isanewline

 \ \ \ \ \ \ Terms{\isaliteral{2E}{\isachardot}}map\ {\isaliteral{28}{\isacharparenleft}}Ord{\isaliteral{5F}{\isacharunderscore}}List{\isaliteral{2E}{\isachardot}}insert\ Term{\isaliteral{5F}{\isacharunderscore}}Ord{\isaliteral{2E}{\isachardot}}fast{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}ord\ t{\isaliteral{29}{\isacharparenright}}\ thy\isanewline

 \ \ \ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \isanewline

 \ \ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \begin{isamarkuptext}%

 Type \verb|term Ord_List.T| is used for reasonably

   efficient representation of a set of terms: all operations are

   linear in the number of stored elements.  Here we assume that users

   of this module do not care about the declaration order, since that

   data structure forces its own arrangement of elements.

   Observe how the \verb|merge| operation joins the data slots of

   the two constituents: \verb|Ord_List.union| prevents duplication of

   common data from different branches, thus avoiding the danger of

   exponential blowup.  Plain list append etc.\ must never be used for

   theory data merges!

   \medskip Our intended invariant is achieved as follows:

   \begin{enumerate}

   \item \verb|Wellformed_Terms.add| only admits terms that have passed

   the \verb|Sign.cert_term| check of the given theory at that point.

   \item Wellformedness in the sense of \verb|Sign.cert_term| is

   monotonic wrt.\ the sub-theory relation.  So our data can move

   upwards in the hierarchy (via extension or merges), and maintain

   wellformedness without further checks.

   \end{enumerate}

   Note that all basic operations of the inference kernel (which

   includes \verb|Sign.cert_term|) observe this monotonicity principle,

   but other user-space tools don't.  For example, fully-featured

   type-inference via \verb|Syntax.check_term| (cf.\

   \secref{sec:term-check}) is not necessarily monotonic wrt.\ the

   background theory, since constraints of term constants can be

   modified by later declarations, for example.

   In most cases, user-space context data does not have to take such

   invariants too seriously.  The situation is different in the

   implementation of the inference kernel itself, which uses the very

   same data mechanisms for types, constants, axioms etc.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsection{Configuration options \label{sec:config-options}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 A \emph{configuration option} is a named optional value of

   some basic type (Boolean, integer, string) that is stored in the

   context.  It is a simple application of general context data

   (\secref{sec:context-data}) that is sufficiently common to justify

   customized setup, which includes some concrete declarations for

   end-users using existing notation for attributes (cf.\

   \secref{sec:attributes}).

   For example, the predefined configuration option \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} controls output of explicit type constraints for

   variables in printed terms (cf.\ \secref{sec:read-print}).  Its

   value can be modified within Isar text like this:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{declare}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

 \ \ %

 \isamarkupcmt{declaration within (local) theory context%

 }

 \isanewline

 \isanewline

 \isacommand{notepad}\isamarkupfalse%

 \isanewline

 \isakeyword{begin}\isanewline

 %

 \isadelimproof

 \ \ %

 \endisadelimproof

 %

 \isatagproof

 \isacommand{note}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

 \ \ \ \ %

 \isamarkupcmt{declaration within proof (forward mode)%

 }

 %

 \endisatagproof

 {\isafoldproof}%

 %

 \isadelimproof

 \isanewline

 %

 \endisadelimproof

 \ \ \isacommand{term}\isamarkupfalse%

 \ x\isanewline

 %

 \isadelimproof

 \isanewline

 \ \ %

 \endisadelimproof

 %

 \isatagproof

 \isacommand{have}\isamarkupfalse%

 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

 \ \ \ \ \isacommand{using}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

 \ \ \ \ \ \ %

 \isamarkupcmt{declaration within proof (backward mode)%

 }

 \isanewline

 \ \ \ \ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

 %

 \endisatagproof

 {\isafoldproof}%

 %

 \isadelimproof

 \isanewline

 %

 \endisadelimproof

 \isacommand{end}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 Configuration options that are not set explicitly hold a

   default value that can depend on the application context.  This

   allows to retrieve the value from another slot within the context,

   or fall back on a global preference mechanism, for example.

   The operations to declare configuration options and get/map their

   values are modeled as direct replacements for historic global

   references, only that the context is made explicit.  This allows

   easy configuration of tools, without relying on the execution order

   as required for old-style mutable references.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML}{Config.get}\verb|Config.get: Proof.context -> 'a Config.T -> 'a| \\

   \indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\

   \indexdef{}{ML}{Attrib.setup\_config\_bool}\verb|Attrib.setup_config_bool: binding -> (Context.generic -> bool) ->|\isasep\isanewline%

 \verb|  bool Config.T| \\

   \indexdef{}{ML}{Attrib.setup\_config\_int}\verb|Attrib.setup_config_int: binding -> (Context.generic -> int) ->|\isasep\isanewline%

 \verb|  int Config.T| \\

   \indexdef{}{ML}{Attrib.setup\_config\_real}\verb|Attrib.setup_config_real: binding -> (Context.generic -> real) ->|\isasep\isanewline%

 \verb|  real Config.T| \\

   \indexdef{}{ML}{Attrib.setup\_config\_string}\verb|Attrib.setup_config_string: binding -> (Context.generic -> string) ->|\isasep\isanewline%

 \verb|  string Config.T| \\

   \end{mldecls}

   \begin{description}

   \item \verb|Config.get|~\isa{ctxt\ config} gets the value of

   \isa{config} in the given context.

   \item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context

   by updating the value of \isa{config}.

   \item \isa{config\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.setup_config_bool|~\isa{name\ default} creates a named configuration option of type \verb|bool|, with the given \isa{default} depending on the application

   context.  The resulting \isa{config} can be used to get/map its

   value in a given context.  There is an implicit update of the

   background theory that registers the option as attribute with some

   concrete syntax.

   \item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for

   types \verb|int| and \verb|string|, respectively.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isatagmlex

 %

 \begin{isamarkuptext}%

 The following example shows how to declare and use a

   Boolean configuration option called \isa{my{\isaliteral{5F}{\isacharunderscore}}flag} with constant

   default value \verb|false|.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlex

 {\isafoldmlex}%

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ val\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}bool\ %

 \isaantiq

 binding\ my{\isaliteral{5F}{\isacharunderscore}}flag{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \begin{isamarkuptext}%

 Now the user can refer to \hyperlink{attribute.my-flag}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}flag}}} in

   declarations, while ML tools can retrieve the current value from the

   context via \verb|Config.get|.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ %

 \isaantiq

 context{}%

 \endisaantiq

 \ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 \isanewline

 \isanewline

 \isacommand{declare}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

 %

 \isadelimML

 \isanewline

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ %

 \isaantiq

 context{}%

 \endisaantiq

 \ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 \isanewline

 %

 \endisadelimML

 \isanewline

 \isacommand{notepad}\isamarkupfalse%

 \isanewline

 \isakeyword{begin}\isanewline

 %

 \isadelimproof

 \ \ %

 \endisadelimproof

 %

 \isatagproof

 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

 \isanewline

 \ \ \ \ \isacommand{note}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%

 \endisatagproof

 {\isafoldproof}%

 %

 \isadelimproof

 \isanewline

 %

 \endisadelimproof

 %

 \isadelimML

 \ \ \ \ %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ %

 \isaantiq

 context{}%

 \endisaantiq

 \ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 \isanewline

 %

 \endisadelimML

 %

 \isadelimproof

 \ \ %

 \endisadelimproof

 %

 \isatagproof

 \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

 %

 \endisatagproof

 {\isafoldproof}%

 %

 \isadelimproof

 \isanewline

 %

 \endisadelimproof

 %

 \isadelimML

 \ \ %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}Config{\isaliteral{2E}{\isachardot}}get\ %

 \isaantiq

 context{}%

 \endisaantiq

 \ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 \isanewline

 %

 \endisadelimML

 \isacommand{end}\isamarkupfalse%

 %

 \begin{isamarkuptext}%

 Here is another example involving ML type \verb|real|

   (floating-point numbers).%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ val\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}real\ %

 \isaantiq

 binding\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 \isanewline

 \isanewline

 \isacommand{declare}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

 \isacommand{declare}\isamarkupfalse%

 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isaliteral{2E}{\isachardot}}{\isadigit{9}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%

 \isamarkupsection{Names \label{sec:names}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 In principle, a name is just a string, but there are various

   conventions for representing additional structure.  For example,

   ``\isa{Foo{\isaliteral{2E}{\isachardot}}bar{\isaliteral{2E}{\isachardot}}baz}'' is considered as a long name consisting of

   qualifier \isa{Foo{\isaliteral{2E}{\isachardot}}bar} and base name \isa{baz}.  The

   individual constituents of a name may have further substructure,

   e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single

   symbol.

   \medskip Subsequently, we shall introduce specific categories of

   names.  Roughly speaking these correspond to logical entities as

   follows:

   \begin{itemize}

   \item Basic names (\secref{sec:basic-name}): free and bound

   variables.

   \item Indexed names (\secref{sec:indexname}): schematic variables.

   \item Long names (\secref{sec:long-name}): constants of any kind

   (type constructors, term constants, other concepts defined in user

   space).  Such entities are typically managed via name spaces

   (\secref{sec:name-space}).

   \end{itemize}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsection{Strings of symbols \label{sec:symbols}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 A \emph{symbol} constitutes the smallest textual unit in

   Isabelle --- raw ML characters are normally not encountered at all!

   Isabelle strings consist of a sequence of symbols, represented as a

   packed string or an exploded list of strings.  Each symbol is in

   itself a small string, which has either one of the following forms:

   \begin{enumerate}

   \item a single ASCII character ``\isa{c}'', for example

   ``\verb,a,'',

   \item a codepoint according to UTF8 (non-ASCII byte sequence),

   \item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',

   for example ``\verb,\,\verb,<alpha>,'',

   \item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',

   for example ``\verb,\,\verb,<^bold>,'',

   \item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''

   where \isa{text} consists of printable characters excluding

   ``\verb,.,'' and ``\verb,>,'', for example

   ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',

   \item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example

   ``\verb,\,\verb,<^raw42>,''.

   \end{enumerate}

   The \isa{ident} syntax for symbol names is \isa{letter\ {\isaliteral{28}{\isacharparenleft}}letter\ {\isaliteral{7C}{\isacharbar}}\ digit{\isaliteral{29}{\isacharparenright}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}}, where \isa{letter\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Za{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}z} and \isa{digit\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\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 letter, which means it may occur within regular

   Isabelle identifiers.

   The character set underlying Isabelle symbols is 7-bit ASCII, but

   8-bit character sequences are passed-through unchanged.  Unicode/UCS

   data in UTF-8 encoding is processed in a non-strict fashion, such

   that well-formed code sequences are recognized

   accordingly.\footnote{Note that ISO-Latin-1 differs from UTF-8 only

   in some special punctuation characters that even have replacements

   within the standard collection of Isabelle symbols.  Text consisting

   of ASCII plus accented letters can be processed in either encoding.}

   Unicode provides its own collection of mathematical symbols, but

   within the core Isabelle/ML world there is no link to the standard

   collection of Isabelle regular symbols.

   \medskip Output of Isabelle symbols depends on the print mode

   (\secref{print-mode}).  For example, the standard {\LaTeX} setup of

   the Isabelle document preparation system would present

   ``\verb,\,\verb,<alpha>,'' as \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, and

   ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  On-screen rendering usually works by mapping a finite

   subset of Isabelle symbols to suitable Unicode characters.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol = string| \\

   \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\

   \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\

   \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\

   \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\

   \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\

   \end{mldecls}

   \begin{mldecls}

   \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\

   \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\

   \end{mldecls}

   \begin{description}

   \item Type \verb|Symbol.symbol| represents individual Isabelle

   symbols.

   \item \verb|Symbol.explode|~\isa{str} produces a symbol list

   from the packed form.  This function supersedes \verb|String.explode| for virtually all purposes of manipulating text in

   Isabelle!\footnote{The runtime overhead for exploded strings is

   mainly that of the list structure: individual symbols that happen to

   be a singleton string do not require extra memory in Poly/ML.}

   \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 Type \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.UTF8|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.

   \item \verb|Symbol.decode| converts the string representation of a

   symbol into the datatype version.

   \end{description}

   \paragraph{Historical note.} In the original SML90 standard the

   primitive ML type \verb|char| did not exists, and the \verb|explode: string -> string list| operation would produce a list of

   singleton strings as does \verb|raw_explode: string -> string list|

   in Isabelle/ML today.  When SML97 came out, Isabelle did not adopt

   its slightly anachronistic 8-bit characters, but the idea of

   exploding a string into a list of small strings was extended to

   ``symbols'' as explained above.  Thus Isabelle sources can refer to

   an infinite store of user-defined symbols, without having to worry

   about the multitude of Unicode encodings.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isamarkupsubsection{Basic names \label{sec:basic-name}%

 }

 \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: 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{\isaliteral{5F}{\isacharunderscore}}}, with Skolem versions \isa{foo{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5F}{\isacharunderscore}}} and \isa{foo{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5F}{\isacharunderscore}}}, respectively.

   These special versions provide copies of the basic name space, apart

   from anything that normally appears in the user text.  For example,

   system generated variables in Isar proof contexts are usually marked

   as internal, which prevents mysterious names like \isa{xaa} to

   appear in human-readable text.

   \medskip Manipulating binding scopes often requires on-the-fly

   renamings.  A \emph{name context} contains a collection of already

   used names.  The \isa{declare} operation adds names to the

   context.

   The \isa{invents} operation derives a number of fresh names from

   a given starting point.  For example, the first three names derived

   from \isa{a} are \isa{a}, \isa{b}, \isa{c}.

   The \isa{variants} operation produces fresh names by

   incrementing tentative names as base-26 numbers (with digits \isa{a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\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

   step picks the next unused variant from this sequence.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\

   \indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\

   \end{mldecls}

   \begin{mldecls}

   \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\

   \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\

   \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\

   \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\

   \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\

   \end{mldecls}

   \begin{mldecls}

   \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> 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 Type \verb|Name.context| represents the context of already

   used names; the initial value is \verb|Name.context|.

   \item \verb|Name.declare|~\isa{name} enters a used name into the

   context.

   \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.

   \item \verb|Name.variant|~\isa{name\ context} produces a fresh

   variant of \isa{name}; the result is declared to the context.

   \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context

   of declared type and term variable names.  Projecting a proof

   context down to a primitive name context is occasionally useful when

   invoking lower-level operations.  Regular management of ``fresh

   variables'' is done by suitable operations of structure \verb|Variable|, which is also able to provide an official status of

   ``locally fixed variable'' within the logical environment (cf.\

   \secref{sec:variables}).

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isatagmlex

 %

 \begin{isamarkuptext}%

 The following simple examples demonstrate how to produce

   fresh names from the initial \verb|Name.context|.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlex

 {\isafoldmlex}%

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ Name{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}b{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \isanewline

 \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}xa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \begin{isamarkuptext}%

 \medskip The same works relatively to the formal context as

   follows.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 \isacommand{locale}\isamarkupfalse%

 \ ex\ {\isaliteral{3D}{\isacharequal}}\ \isakeyword{fixes}\ a\ b\ c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline

 \isakeyword{begin}\isanewline

 %

 \isadelimML

 \isanewline

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ val\ names\ {\isaliteral{3D}{\isacharequal}}\ Variable{\isaliteral{2E}{\isachardot}}names{\isaliteral{5F}{\isacharunderscore}}of\ %

 \isaantiq

 context{}%

 \endisaantiq

 {\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \isanewline

 \ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ names\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}g{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}h{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \isanewline

 \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

 \ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 \ \ %

 \isaantiq

 assert{}%

 \endisaantiq

 \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}xa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}ab{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}aa{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}ab{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 \isanewline

 %

 \endisadelimML

 \isanewline

 \isacommand{end}\isamarkupfalse%

 %

 \isamarkupsubsection{Indexed names \label{sec:indexname}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 An \emph{indexed name} (or \isa{indexname}) is a pair of a basic

   name and a natural number.  This representation allows efficient

   renaming by incrementing the second component only.  The canonical

   way to rename two collections of indexnames apart from each other is

   this: determine the maximum index \isa{maxidx} of the first

   collection, then increment all indexes of the second collection by

   \isa{maxidx\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}}; the maximum index of an empty collection is

   \isa{{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}}.

   Occasionally, basic names are injected into the same pair type of

   indexed names: then \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}} is used to encode the basic

   name \isa{x}.

   \medskip Isabelle syntax observes the following rules for

   representing an indexname \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}} as a packed string:

   \begin{itemize}

   \item \isa{{\isaliteral{3F}{\isacharquery}}x} if \isa{x} does not end with a digit and \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}},

   \item \isa{{\isaliteral{3F}{\isacharquery}}xi} if \isa{x} does not end with a digit,

   \item \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2E}{\isachardot}}i} otherwise.

   \end{itemize}

   Indexnames may acquire large index numbers after several maxidx

   shifts have been applied.  Results are usually normalized towards

   \isa{{\isadigit{0}}} at certain checkpoints, notably at the end of a proof.

   This works by producing variants of the corresponding basic name

   components.  For example, the collection \isa{{\isaliteral{3F}{\isacharquery}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{7}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{4}}{\isadigit{2}}}

   becomes \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}xa{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}xb}.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML type}{indexname}\verb|type indexname = string * int| \\

   \end{mldecls}

   \begin{description}

   \item Type \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{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}} is used to inject basic names into this type.  Other negative

   indexes should not be used.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isamarkupsubsection{Long names \label{sec:long-name}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 A \emph{long name} consists of a sequence of non-empty name

   components.  The packed representation uses a dot as separator, as

   in ``\isa{A{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}c}''.  The last component is called \emph{base

   name}, the remaining prefix is called \emph{qualifier} (which may be

   empty).  The qualifier can be understood as the access path to the

   named entity while passing through some nested block-structure,

   although our free-form long names do not really enforce any strict

   discipline.

   For example, an item named ``\isa{A{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}c}'' may be understood as

   a local entity \isa{c}, within a local structure \isa{b},

   within a global structure \isa{A}.  In practice, long names

   usually represent 1--3 levels of qualification.  User ML code should

   not make any assumptions about the particular structure of long

   names!

   The empty name is commonly used as an indication of unnamed

   entities, or entities that are not entered into the corresponding

   name space, whenever this makes any sense.  The basic operations on

   long names map empty names again to empty names.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\

   \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\

   \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\

   \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\

   \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\

   \end{mldecls}

   \begin{description}

   \item \verb|Long_Name.base_name|~\isa{name} returns the base name

   of a long name.

   \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier

   of a long name.

   \item \verb|Long_Name.append|~\isa{name\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ name\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} appends two long

   names.

   \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string

   representation and the explicit list form of long names.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isamarkupsubsection{Name spaces \label{sec:name-space}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 A \isa{name\ space} manages a collection of long names,

   together with a mapping between partially qualified external names

   and fully qualified internal names (in both directions).  Note that

   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 the accesses

   determined by a given binding, and a naming policy from the context.

   \medskip A \isa{binding} specifies details about the prospective

   long name of a newly introduced formal entity.  It consists of a

   base name, prefixes for qualification (separate ones for system

   infrastructure and user-space mechanisms), a slot for the original

   source position, and some additional flags.

   \medskip A \isa{naming} provides some additional details for

   producing a long name from a binding.  Normally, the naming is

   implicit in the theory or proof context.  The \isa{full}

   operation (and its variants for different context types) produces a

   fully qualified internal name to be entered into a name space.  The

   main equation of this ``chemical reaction'' when binding new

   entities in a context is as follows:

   \medskip

   \begin{tabular}{l}

   \isa{binding\ {\isaliteral{2B}{\isacharplus}}\ naming\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ long\ name\ {\isaliteral{2B}{\isacharplus}}\ name\ space\ accesses}

   \end{tabular}

   \bigskip As a general principle, there is a separate name space for

   each kind of formal entity, e.g.\ fact, logical constant, type

   constructor, type class.  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 constructor, and type class.

   There are common schemes to name derived entities systematically

   according to the name of the main logical entity involved, e.g.\

   fact \isa{c{\isaliteral{2E}{\isachardot}}intro} for a canonical introduction rule 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 a type constructor or type

   class should get an additional suffix in addition to the usual

   qualification.  This leads to the following conventions for derived

   names:

   \medskip

   \begin{tabular}{ll}

   logical entity & fact name \\\hline

   constant \isa{c} & \isa{c{\isaliteral{2E}{\isachardot}}intro} \\

   type \isa{c} & \isa{c{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{2E}{\isachardot}}intro} \\

   class \isa{c} & \isa{c{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}intro} \\

   \end{tabular}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isatagmlref

 %

 \begin{isamarkuptext}%

 \begin{mldecls}

   \indexdef{}{ML type}{binding}\verb|type binding| \\

   \indexdef{}{ML}{Binding.empty}\verb|Binding.empty: binding| \\

   \indexdef{}{ML}{Binding.name}\verb|Binding.name: string -> binding| \\

   \indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\

   \indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\

   \indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\

   \indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\

   \end{mldecls}

   \begin{mldecls}

   \indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\

   \indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\

   \indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\

   \indexdef{}{ML}{Name\_Space.full\_name}\verb|Name_Space.full_name: Name_Space.naming -> binding -> string| \\

   \end{mldecls}

   \begin{mldecls}

   \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\

   \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\

   \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\

   \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline%

 \verb|  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\

   \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\

   \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\

   \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|

   \end{mldecls}

   \begin{description}

   \item Type \verb|binding| represents the abstract concept of

   name bindings.

   \item \verb|Binding.empty| is the empty binding.

   \item \verb|Binding.name|~\isa{name} produces a binding with base

   name \isa{name}.  Note that this lacks proper source position

   information; see also the ML antiquotation \hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}.

   \item \verb|Binding.qualify|~\isa{mandatory\ name\ binding}

   prefixes qualifier \isa{name} to \isa{binding}.  The \isa{mandatory} flag tells if this name component always needs to be

   given in name space accesses --- this is mostly \isa{false} in

   practice.  Note that this part of qualification is typically used in

   derived specification mechanisms.

   \item \verb|Binding.prefix| is similar to \verb|Binding.qualify|, but

   affects the system prefix.  This part of extra qualification is

   typically used in the infrastructure for modular specifications,

   notably ``local theory targets'' (see also \chref{ch:local-theory}).

   \item \verb|Binding.conceal|~\isa{binding} indicates that the

   binding shall refer to an entity that serves foundational purposes

   only.  This flag helps to mark implementation details of

   specification mechanism etc.  Other tools should not depend on the

   particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|).

   \item \verb|Binding.str_of|~\isa{binding} produces a string

   representation for human-readable output, together with some formal

   markup that might get used in GUI front-ends, for example.

   \item Type \verb|Name_Space.naming| represents the abstract

   concept of a naming policy.

   \item \verb|Name_Space.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|Name_Space.add_path|~\isa{path\ naming} augments the

   naming policy by extending its path component.

   \item \verb|Name_Space.full_name|~\isa{naming\ binding} turns a

   name binding (usually a basic name) into the fully qualified

   internal name, according to the given naming policy.

   \item Type \verb|Name_Space.T| represents name spaces.

   \item \verb|Name_Space.empty|~\isa{kind} and \verb|Name_Space.merge|~\isa{{\isaliteral{28}{\isacharparenleft}}space\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ space\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} are the canonical operations for

   maintaining name spaces according to theory data management

   (\secref{sec:context-data}); \isa{kind} is a formal comment

   to characterize the purpose of a name space.

   \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into

   the name space, with external accesses determined by the naming

   policy.

   \item \verb|Name_Space.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|Name_Space.full_name| and \verb|Name_Space.declare|

   (or their derivatives for \verb|theory| and

   \verb|Proof.context|).

   \item \verb|Name_Space.extern|~\isa{ctxt\ space\ name} externalizes a

   (fully qualified) internal name.

   This operation is mostly for printing!  User code should not rely on

   the precise result too much.

   \item \verb|Name_Space.is_concealed|~\isa{space\ name} indicates

   whether \isa{name} refers to a strictly private entity that

   other tools are supposed to ignore!

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlref

 {\isafoldmlref}%

 %

 \isadelimmlref

 %

 \endisadelimmlref

 %

 \isadelimmlantiq

 %

 \endisadelimmlantiq

 %

 \isatagmlantiq

 %

 \begin{isamarkuptext}%

 \begin{matharray}{rcl}

   \indexdef{}{ML antiquotation}{binding}\hypertarget{ML antiquotation.binding}{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   \end{matharray}

   \begin{railoutput}

 \rail@begin{1}{}

 \rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[]

 \rail@nont{\isa{name}}[]

 \rail@end

 \end{railoutput}

   \begin{description}

   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}binding\ name{\isaliteral{7D}{\isacharbraceright}}} produces a binding with base name

   \isa{name} and the source position taken from the concrete

   syntax of this antiquotation.  In many situations this is more

   appropriate than the more basic \verb|Binding.name| function.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlantiq

 {\isafoldmlantiq}%

 %

 \isadelimmlantiq

 %

 \endisadelimmlantiq

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isatagmlex

 %

 \begin{isamarkuptext}%

 The following example yields the source position of some

   concrete binding inlined into the text:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \endisatagmlex

 {\isafoldmlex}%

 %

 \isadelimmlex

 %

 \endisadelimmlex

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Binding{\isaliteral{2E}{\isachardot}}pos{\isaliteral{5F}{\isacharunderscore}}of\ %

 \isaantiq

 binding\ here{}%

 \endisaantiq

 \ {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \begin{isamarkuptext}%

 \medskip That position can be also printed in a message as

   follows:%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \isatagML

 \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}\isamarkupfalse%

 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

 \ \ writeln\isanewline

 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Look\ here{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ Position{\isaliteral{2E}{\isachardot}}str{\isaliteral{5F}{\isacharunderscore}}of\ {\isaliteral{28}{\isacharparenleft}}Binding{\isaliteral{2E}{\isachardot}}pos{\isaliteral{5F}{\isacharunderscore}}of\ %

 \isaantiq

 binding\ here{}%

 \endisaantiq

 {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

 {\isaliteral{2A7D}{\isacharverbatimclose}}%

 \endisatagML

 {\isafoldML}%

 %

 \isadelimML

 %

 \endisadelimML

 %

 \begin{isamarkuptext}%

 This illustrates a key virtue of formalized bindings as

   opposed to raw specifications of base names: the system can use this

   additional information for feedback given to the user (error

   messages etc.).%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isatagtheory

 \isacommand{end}\isamarkupfalse%

 %

 \endisatagtheory

 {\isafoldtheory}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 \isanewline

 \end{isabellebody}%

 %%% Local Variables:

 %%% mode: latex

 %%% TeX-master: "root"

 %%% End: