A logical context represents the background that is taken for

   A logical context represents the background that is required for

   granted when formulating statements and composing proofs.  It acts

   formulating statements and composing proofs.  It acts as a medium to

   as a medium to produce formal content, depending on earlier material

   produce formal content, depending on earlier material (declarations,

   (declarations, results etc.).

   results etc.).

   In particular, derivations within the primitive Pure logic can be

   For example, derivations within the Isabelle/Pure logic can be

   described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, meaning that a

   described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, which means that a

   keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories support type

   keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories can be

   constructors and schematic polymorphism of constants and axioms,

   liberal about supporting type constructors and schematic

   while the inner calculus of @{text "\<Gamma> \<turnstile> \<phi>"} is limited to Simple

   polymorphism of constants and axioms, while the inner calculus of

   Type Theory (with fixed type variables in the assumptions).

   @{text "\<Gamma> \<turnstile> \<phi>"} is strictly limited to Simple Type Theory (with

   fixed type variables in the assumptions).

   transferred into a larger context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}

   transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta>

   implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' \<supseteq>

   \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'

   \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.

   \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.

   into a smaller context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} implies

   into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}

   @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and @{text "\<Delta> =

   implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and

   \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here, only the

   @{text "\<Delta> = \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here,

   @{text "\<Gamma>"} part is affected.

   only the @{text "\<Gamma>"} part is affected.

   \medskip Isabelle/Isar provides two different notions of abstract

   \medskip By modeling the main characteristics of the primitive

   containers called \emph{theory context} and \emph{proof context},

   @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any

   respectively.  These model the main characteristics of the primitive

   particular logical content, we arrive at the fundamental notions of

   @{text "\<Theta>"} and @{text "\<Gamma>"} above, without subscribing to any

   \emph{theory context} and \emph{proof context} in Isabelle/Isar.

   particular kind of content yet.  Instead, contexts merely impose a

   These implement a certain policy to manage arbitrary \emph{context

   certain policy of managing arbitrary \emph{context data}.  The

   data}.  There is a strongly-typed mechanism to declare new kinds of

   system provides strongly typed mechanisms to declare new kinds of

   Thus the internal bootstrap process of Isabelle/Pure eventually

   The internal bootstrap process of Isabelle/Pure eventually reaches a

   reaches a stage where certain data slots provide the logical content

   stage where certain data slots provide the logical content of @{text

   of @{text "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not

   "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there!

   stop there!  Various additional data slots support all kinds of

   Various additional data slots support all kinds of mechanisms that

   mechanisms that are not necessarily part of the core logic.

   are not necessarily part of the core logic.

   standard proof steps implicitly (cf.\ the @{text "rule"} method).

   standard proof steps implicitly (cf.\ the @{text "rule"} method

   \cite{isabelle-isar-ref}).

   Isabelle is able to bring forth more and more concepts successively.

   In particular, an object-logic like Isabelle/HOL continues the

   \medskip Thus Isabelle/Isar is able to bring forth more and more

   Isabelle/Pure setup by adding specific components for automated

   concepts successively.  In particular, an object-logic like

   reasoning (classical reasoner, tableau prover, structured induction

   Isabelle/HOL continues the Isabelle/Pure setup by adding specific

   etc.) and derived specification mechanisms (inductive predicates,

   components for automated reasoning (classical reasoner, tableau

   recursive functions etc.).  All of this is based on the generic data

   prover, structured induction etc.) and derived specification

   management by theory and proof contexts.

   mechanisms (inductive predicates, recursive functions etc.).  All of

   this is ultimately based on the generic data management by theory

   and proof contexts introduced here.

   Each theory is explicitly named and holds a unique identifier.

   A \emph{theory} is a data container with explicit named and unique

   There is a separate \emph{theory reference} for pointing backwards

   identifier.  Theories are related by a (nominal) sub-theory

   to the enclosing theory context of derived entities.  Theories are

   relation, which corresponds to the dependency graph of the original

   related by a (nominal) sub-theory relation, which corresponds to the

   construction; each theory is derived from a certain sub-graph of

   canonical dependency graph: each theory is derived from a certain

   ancestor theories.

   sub-graph of ancestor theories.  The @{text "merge"} of two theories

   refers to the least upper bound, which actually degenerates into

   The @{text "merge"} operation produces the least upper bound of two

   absorption of one theory into the other, due to the nominal

   theories, which actually degenerates into absorption of one theory

   sub-theory relation this.

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

   mode theory acts like a linear type, where updates invalidate

   theory acts like a linear type, where updates invalidate earlier

   earlier drafts, but theory reference values will be propagated

   versions.  An invalidated draft is called ``stale''.

   automatically.  Thus derived entities that ``belong'' to a draft

   might be transferred spontaneously to a larger context.  An

   invalidated draft is called ``stale''.

   stone that will survive the next update unscathed: both the original

   stone that will survive the next update: both the original and the

   and the changed theory remain valid and are related by the

   changed theory remain valid and are related by the sub-theory

   sub-theory relation.  Checkpointing essentially recovers purely

   relation.  Checkpointing essentially recovers purely functional

   functional theory values, at the expense of some extra internal

   theory values, at the expense of some extra internal bookkeeping.

   bookkeeping.

   graph derived from @{text "Pure"}. Theory @{text "Length"} imports

   graph derived from @{text "Pure"}, with theory @{text "Length"}

   @{text "Nat"} and @{text "List"}.  The theory body consists of a

   importing @{text "Nat"} and @{text "List"}.  The body of @{text

   sequence of updates, working mostly on drafts.  Intermediate

   "Length"} consists of a sequence of updates, working mostly on

   checkpoints may occur as well, due to the history mechanism provided

   drafts.  Intermediate checkpoints may occur as well, due to the

   by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.

   history mechanism provided by the Isar top-level, cf.\

   \secref{sec:isar-toplevel}.

   \caption{Theory definition depending on ancestors}\label{fig:ex-theory}

   \caption{A theory definition depending on ancestors}\label{fig:ex-theory}

   \item @{ML_type theory} represents theory contexts.  This is a

   \item @{ML_type theory} represents theory contexts.  This is

   linear type!  Most operations destroy the old version, which then

   essentially a linear type!  Most operations destroy the original

   becomes ``stale''.

   version, which then becomes ``stale''.

   "thy"} that holds a copy of the same data.  The copy is not related

   "thy"} that holds a copy of the same data.  The result is not

   to the original, which is not touched at all.

   related to the original; the original is unchanched.

   \item @{ML_type theory_ref} represents a sliding reference to a

   \item @{ML_type theory_ref} represents a sliding reference to an

   valid theory --- updates on the original are propagated

   always valid theory; updates on the original are propagated

   "Theory.deref"} may refer to larger contexts.

   "Theory.deref"} may refer to a larger context.

   proof context derived from a given theory.  Modifications to draft

   proof context from a given theory.  Modifications to draft theories

   theories are propagated to the proof context as usual, but there is

   are propagated to the proof context as usual, but there is also an

   also an explicit @{text "transfer"} operation to force

   explicit @{text "transfer"} operation to force resynchronization

   resynchronization with more substantial updates to the underlying

   with more substantial updates to the underlying theory.  The actual

   theory.  The actual context data does not require any special

   context data does not require any special bookkeeping, thanks to the

   bookkeeping, thanks to the lack of destructive features.

   lack of destructive features.

   primitive derivations (cf.\ \secref{sec:thm}) are recorded

   primitive derivations (cf.\ \secref{sec:thms}) are recorded

   Proof contexts may be produced in arbitrary ways, although the

   Proof contexts may be manipulated arbitrarily, although the common

   common discipline is to follow block structure as a mental model: a

   discipline is to follow block structure as a mental model: a given

   given context is extended consecutively, and results are exported

   context is extended consecutively, and results are exported back

   back into the original context.  Note that the Isar proof states

   into the original context.  Note that the Isar proof states model

   model block-structured reasoning explicitly, using a stack of proof

   block-structured reasoning explicitly, using a stack of proof

   contexts, cf.\ \secref{isar-proof-state}.

   contexts internally, cf.\ \secref{sec:isar-proof-state}.

   background theory from @{text "ctxt"}.

   background theory from @{text "ctxt"}, dereferencing its internal

   @{ML_type theory_ref}.

 subsection {* Generic contexts \label{sec:generic-context} *}

 subsection {* Generic contexts *}

   context.  Occasionally, this simplifies uniform treatment of generic

   context.  Occasionally, this enables uniform treatment of generic

   can always be selected, while a proof context may have to be

   can always be selected from the sum, while a proof context might

   constructed by an ad-hoc @{text "init"} operation.

   have to be constructed by an ad-hoc @{text "init"} operation.

   "theory"} and @{ML_type "Proof.context"}, with datatype constructors

   "theory"} and @{ML_type "Proof.context"}, with the datatype

   @{ML "Context.Theory"} and @{ML "Context.Proof"}.

   constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.

   "ProofContext.init"} as required.  Note that this re-initializes the

   "ProofContext.init"} as required (note that this re-initializes the

   context data with each invocation.

   context data with each invocation).

   Both theory and proof contexts manage arbitrary data, which is the

   The main purpose of theory and proof contexts is to manage arbitrary

   main purpose of contexts in the first place.  Data can be declared

   data.  New data types can be declared incrementally at compile time.

   incrementally at compile --- Isabelle/Pure and major object-logics

   There are separate declaration mechanisms for any of the three kinds

   are bootstrapped that way.

   of contexts: theory, proof, generic.

   maintained in correspondence to the linear evolution of theory

   maintained in direct correspondence to the linear evolution of

   values, or explicit copies.\footnote{Most existing instances of

   theory values, including explicit copies.\footnote{Most existing

   destructive theory data are merely historical relics (e.g.\ the

   instances of destructive theory data are merely historical relics

   destructive theorem storage, and destructive hints for the

   (e.g.\ the destructive theorem storage, and destructive hints for

   Simplifier and Classical rules).}  A theory data declaration needs

   the Simplifier and Classical rules).}  A theory data declaration

   to implement the following specification:

   needs to implement the following specification (depending on type

   @{text "T"}):

   \paragraph{Proof context data} is purely functional.  It is declared

   \paragraph{Proof context data} is purely functional.  A declaration

   by implementing the following specification:

   needs to implement the following specification:

   value from the given background theory.  The rest is analogous to

   value from the given background theory.  The remainder is analogous

   (pure) theory data.

   to theory data.

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

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

   The declaration is essentially the same as for pure theory data,

   and proof data.  The declaration is essentially the same as for

   without @{text "copy"} (it is always the identity).  The @{text

   (pure) theory data, without @{text "copy"}, though.  The @{text

   "init"} operation for proof contexts selects the current data value

   "init"} operation for proof contexts merely selects the current data

   from the background theory.

   value from the background theory.

   slot within a context.  By keeping these operations private, a

   slot of a context.  By keeping these operations private, a component

   component may maintain abstract values authentically, without other

   may maintain abstract values authentically, without other components

   components interfering.

   interfering.

   argument structure.  The result structure provides init and access

   argument structure.  The resulting structure provides data init and

   operations as described above.

   access operations as described above.

 text {* Named entities of different kinds (logical constant, type,

 text {*

 type class, theorem, method etc.) live in separate name spaces.  It is

   By general convention, each kind of formal entities (logical

 usually clear from the occurrence of a name which kind of entity it

   constant, type, type class, theorem, method etc.) lives in a

 refers to.  For example, proof method @{text "foo"} vs.\ theorem

   separate name space.  It is usually clear from the syntactic context

 @{text "foo"} vs.\ logical constant @{text "foo"} are easily

   of a name, which kind of entity it refers to.  For example, proof

 distinguished by means of the syntactic context.  A notable exception

   method @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical

 are logical identifiers within a term (\secref{sec:terms}): constants,

   constant @{text "foo"} are easily distinguished thanks to the design

 fixed variables, and bound variables all share the same identifier

   of the concrete outer syntax.  A notable exception are logical

 syntax, but are distinguished by their scope.

   identifiers within a term (\secref{sec:terms}): constants, fixed

   variables, and bound variables all share the same identifier syntax,

 Each name space is organized as a collection of \emph{qualified

   but are distinguished by their scope.

 names}, which consist of a sequence of basic name components separated

 by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}

   Name spaces are organized uniformly, as a collection of qualified

 are examples for valid qualified names.  Name components are

   names consisting of a sequence of basic name components separated by

 subdivided into \emph{symbols}, which constitute the smallest textual

   dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}

 unit in Isabelle --- raw characters are normally not encountered

   are examples for qualified names.

 directly. *}

   Despite the independence of names of different kinds, certain naming

   conventions may relate them to each other.  For example, a constant

   @{text "foo"} could be accompanied with theorems @{text

   "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The same

   could happen for a type @{text "foo"}, but this is apt to cause

   clashes in the theorem name space!  To avoid this, there is an

   additional convention to add a suffix that determines the original

   kind.  For example, constant @{text "foo"} could associated with

   theorem @{text "foo.intro"}, type @{text "foo"} with theorem @{text

   "foo_type.intro"}, and type class @{text "foo"} with @{text

   "foo_class.intro"}.

   \medskip Name components are subdivided into \emph{symbols}, which

   constitute the smallest textual unit in Isabelle --- raw characters

   are normally not encountered.

 *}

 text {* Isabelle strings consist of a sequence of

 text {*

 symbols\glossary{Symbol}{The smallest unit of text in Isabelle,

   Isabelle strings consist of a sequence of

 subsumes plain ASCII characters as well as an infinite collection of

   symbols\glossary{Symbol}{The smallest unit of text in Isabelle,

 named symbols (for greek, math etc.).}, which are either packed as an

   subsumes plain ASCII characters as well as an infinite collection of

 actual @{text "string"}, or represented as a list.  Each symbol is in

   named symbols (for greek, math etc.).}, which are either packed as

 itself a small string of the following form:

   an actual @{text "string"}, or represented as a list.  Each symbol

   is in itself a small string of the following form:

 \begin{enumerate}

   \begin{enumerate}

 \item either a singleton ASCII character ``@{text "c"}'' (with

 character code 0--127), for example ``\verb,a,'',

   \item either a singleton ASCII character ``@{text "c"}'' (with

   character code 0--127), for example ``\verb,a,'',

 \item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',

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

   \item or a regular symbol ``\verb,\,\verb,<,@{text

   "ident"}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',

 \item or a control symbol ``\verb,\,\verb,<^,@{text

 "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',

   \item or a control symbol ``\verb,\,\verb,<^,@{text

   "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',

 \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text

 "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any

   \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text

 printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or

   "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII

 non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',

   character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII

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

 \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text

 "nnn"}\verb,>, where @{text "nnn"} are digits, for example

   \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text

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

   "nnn"}\verb,>, where @{text "nnn"} are digits, for example

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

 \end{enumerate}

   \end{enumerate}

 The @{text "ident"} syntax for symbol names is @{text "letter (letter

 | digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text

   The @{text "ident"} syntax for symbol names is @{text "letter

 "digit = 0..9"}.  There are infinitely many regular symbols and

   (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and

 control symbols available, but a certain collection of standard

   @{text "digit = 0..9"}.  There are infinitely many regular symbols

 symbols is treated specifically.  For example,

   and control symbols available, but a certain collection of standard

 ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,

   symbols is treated specifically.  For example,

 which means it may occur within regular Isabelle identifier syntax.

   ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,

   which means it may occur within regular Isabelle identifier syntax.

 Output of symbols depends on the print mode (\secref{sec:print-mode}).

 For example, the standard {\LaTeX} setup of the Isabelle document

   Output of symbols depends on the print mode

 preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text

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

 "\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text

   of the Isabelle document preparation system would present

 "\<^bold>\<alpha>"}.

   ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and

   ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text

 \medskip It is important to note that the character set underlying

   "\<^bold>\<alpha>"}.

 Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are

 passed through transparently, Isabelle may easily process actual

   \medskip It is important to note that the character set underlying

 Unicode/UCS data (using the well-known UTF-8 encoding, for example).

   Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are

 Unicode provides its own collection of mathematical symbols, but there

   passed through transparently, Isabelle may easily process

 is presently no link to Isabelle's named ones; both kinds of symbols

   Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides

 coexist independently. *}

   its own collection of mathematical symbols, but there is no built-in

   link to the ones of Isabelle.

 *}

   @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\

   @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]

   \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type

   \item @{ML_type "Symbol.symbol"} represents Isabelle symbols.  This

   is merely an alias for @{ML_type "string"}, but emphasizes the

   type is an alias for @{ML_type "string"}, but emphasizes the

   the packed form usually encountered as user input.  This function

   the packed form that is encountered in most practical situations.

   replaces @{ML "String.explode"} for virtually all purposes of

   This function supercedes @{ML "String.explode"} for virtually all

   manipulating text in Isabelle!  Plain @{ML "implode"} may be used

   purposes of manipulating text in Isabelle!  Plain @{ML "implode"}

   for the reverse operation.

   may still be used for the reverse operation.

   convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.

   conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.

   the different kinds of symbols explicitly as @{ML "Symbol.Char"},

   the different kinds of symbols explicitly with constructors @{ML

   @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.

   "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML

   "Symbol.Raw"}.

   symbol into the explicit datatype version.

   symbol into the datatype version.

 *}

   Qualified names are constructed according to implicit naming

   principles of the present context.

 text %mlref FIXME

   The last component is called \emph{base name}; the remaining prefix

   of qualification may be empty.

   Some practical conventions help to organize named entities more

   systematically:

   \begin{itemize}

   \item Names are qualified first by the theory name, second by an

   optional ``structure''.  For example, a constant @{text "c"}

   declared as part of a certain structure @{text "b"} (say a type

   definition) in theory @{text "A"} will be named @{text "A.b.c"}

   internally.

   \item

   \item

   \item

   \item

   \end{itemize}

   Names of different kinds of entities are basically independent, but

   some practical naming conventions relate them to each other.  For

   example, a constant @{text "foo"} may be accompanied with theorems

   @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.

   The same may happen for a type @{text "foo"}, which is then apt to

   cause clashes in the theorem name space!  To avoid this, we

   occasionally follow an additional convention of suffixes that

   determine the original kind of entity that a name has been derived.

   For example, constant @{text "foo"} is associated with theorem

   @{text "foo.intro"}, type @{text "foo"} with theorem @{text

   "foo_type.intro"}, and type class @{text "foo"} with @{text

   "foo_class.intro"}.

 *}

 subsection {* Print modes *}

 subsection {* Print modes \label{sec:print-mode} *}