
diff -r 861e06a047c5 -r 19363c70b5c4 doc-src/IsarRef/Thy/document/Generic.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon May 05 15:23:21 2008 +0200
@@ -0,0 +1,2062 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Generic}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Generic\isanewline
+\isakeyword{imports}\ CPure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Generic tools and packages \label{ch:gen-tools}%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Specification commands%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Derived specifications%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+    \indexdef{}{command}{axiomatization}\mbox{\isa{\isacommand{axiomatization}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
+    \indexdef{}{command}{definition}\mbox{\isa{\isacommand{definition}}} & : & \isarkeep{local{\dsh}theory} \\
+    \indexdef{}{attribute}{defn}\mbox{\isa{defn}} & : & \isaratt \\
+    \indexdef{}{command}{abbreviation}\mbox{\isa{\isacommand{abbreviation}}} & : & \isarkeep{local{\dsh}theory} \\
+    \indexdef{}{command}{print-abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{command}{notation}\mbox{\isa{\isacommand{notation}}} & : & \isarkeep{local{\dsh}theory} \\
+    \indexdef{}{command}{no-notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
+  \end{matharray}
+
+  These specification mechanisms provide a slightly more abstract view
+  than the underlying primitives of \mbox{\isa{\isacommand{consts}}}, \mbox{\isa{\isacommand{defs}}} (see \secref{sec:consts}), and \mbox{\isa{\isacommand{axioms}}} (see
+  \secref{sec:axms-thms}).  In particular, type-inference is commonly
+  available, and result names need not be given.
+
+  \begin{rail}
+    'axiomatization' target? fixes? ('where' specs)?
+    ;
+    'definition' target? (decl 'where')? thmdecl? prop
+    ;
+    'abbreviation' target? mode? (decl 'where')? prop
+    ;
+    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
+    ;
+
+    fixes: ((name ('::' type)? mixfix? | vars) + 'and')
+    ;
+    specs: (thmdecl? props + 'and')
+    ;
+    decl: name ('::' type)? mixfix?
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{\isacommand{axiomatization}}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}] introduces several constants
+  simultaneously and states axiomatic properties for these.  The
+  constants are marked as being specified once and for all, which
+  prevents additional specifications being issued later on.
+  
+  Note that axiomatic specifications are only appropriate when
+  declaring a new logical system.  Normal applications should only use
+  definitional mechanisms!
+
+  \item [\mbox{\isa{\isacommand{definition}}}~\isa{c\ {\isasymWHERE}\ eq}] produces an
+  internal definition \isa{c\ {\isasymequiv}\ t} according to the specification
+  given as \isa{eq}, which is then turned into a proven fact.  The
+  given proposition may deviate from internal meta-level equality
+  according to the rewrite rules declared as \mbox{\isa{defn}} by the
+  object-logic.  This typically covers object-level equality \isa{x\ {\isacharequal}\ t} and equivalence \isa{A\ {\isasymleftrightarrow}\ B}.  End-users normally need not
+  change the \mbox{\isa{defn}} setup.
+  
+  Definitions may be presented with explicit arguments on the LHS, as
+  well as additional conditions, e.g.\ \isa{f\ x\ y\ {\isacharequal}\ t} instead of
+  \isa{f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t} and \isa{y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u} instead of an
+  unrestricted \isa{g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u}.
+  
+  \item [\mbox{\isa{\isacommand{abbreviation}}}~\isa{c\ {\isasymWHERE}\ eq}] introduces
+  a syntactic constant which is associated with a certain term
+  according to the meta-level equality \isa{eq}.
+  
+  Abbreviations participate in the usual type-inference process, but
+  are expanded before the logic ever sees them.  Pretty printing of
+  terms involves higher-order rewriting with rules stemming from
+  reverted abbreviations.  This needs some care to avoid overlapping
+  or looping syntactic replacements!
+  
+  The optional \isa{mode} specification restricts output to a
+  particular print mode; using ``\isa{input}'' here achieves the
+  effect of one-way abbreviations.  The mode may also include an
+  ``\mbox{\isa{\isakeyword{output}}}'' qualifier that affects the concrete syntax
+  declared for abbreviations, cf.\ \mbox{\isa{\isacommand{syntax}}} in
+  \secref{sec:syn-trans}.
+  
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}] prints all constant abbreviations
+  of the current context.
+  
+  \item [\mbox{\isa{\isacommand{notation}}}~\isa{c\ {\isacharparenleft}mx{\isacharparenright}}] associates mixfix
+  syntax with an existing constant or fixed variable.  This is a
+  robust interface to the underlying \mbox{\isa{\isacommand{syntax}}} primitive
+  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
+  representation of the given entity is retrieved from the context.
+  
+  \item [\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}] is similar to \mbox{\isa{\isacommand{notation}}}, but removes the specified syntax annotation from the
+  present context.
+
+  \end{descr}
+
+  All of these specifications support local theory targets (cf.\
+  \secref{sec:target}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Generic declarations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Arbitrary operations on the background context may be wrapped-up as
+  generic declaration elements.  Since the underlying concept of local
+  theories may be subject to later re-interpretation, there is an
+  additional dependency on a morphism that tells the difference of the
+  original declaration context wrt.\ the application context
+  encountered later on.  A fact declaration is an important special
+  case: it consists of a theorem which is applied to the context by
+  means of an attribute.
+
+  \begin{matharray}{rcl}
+    \indexdef{}{command}{declaration}\mbox{\isa{\isacommand{declaration}}} & : & \isarkeep{local{\dsh}theory} \\
+    \indexdef{}{command}{declare}\mbox{\isa{\isacommand{declare}}} & : & \isarkeep{local{\dsh}theory} \\
+  \end{matharray}
+
+  \begin{rail}
+    'declaration' target? text
+    ;
+    'declare' target? (thmrefs + 'and')
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{declaration}}}~\isa{d}] adds the declaration
+  function \isa{d} of ML type \verb|declaration|, to the current
+  local theory under construction.  In later application contexts, the
+  function is transformed according to the morphisms being involved in
+  the interpretation hierarchy.
+
+  \item [\mbox{\isa{\isacommand{declare}}}~\isa{thms}] declares theorems to the
+  current local theory context.  No theorem binding is involved here,
+  unlike \mbox{\isa{\isacommand{theorems}}} or \mbox{\isa{\isacommand{lemmas}}} (cf.\
+  \secref{sec:axms-thms}), so \mbox{\isa{\isacommand{declare}}} only has the effect
+  of applying attributes as included in the theorem specification.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Local theory targets \label{sec:target}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A local theory target is a context managed separately within the
+  enclosing theory.  Contexts may introduce parameters (fixed
+  variables) and assumptions (hypotheses).  Definitions and theorems
+  depending on the context may be added incrementally later on.  Named
+  contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
+  (cf.\ \secref{sec:class}); the name ``\isa{{\isacharminus}}'' signifies the
+  global theory context.
+
+  \begin{matharray}{rcll}
+    \indexdef{}{command}{context}\mbox{\isa{\isacommand{context}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+    \indexdef{}{command}{end}\mbox{\isa{\isacommand{end}}} & : & \isartrans{local{\dsh}theory}{theory} \\
+  \end{matharray}
+
+  \indexouternonterm{target}
+  \begin{rail}
+    'context' name 'begin'
+    ;
+
+    target: '(' 'in' name ')'
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{\isacommand{context}}}~\isa{c\ {\isasymBEGIN}}] recommences an
+  existing locale or class context \isa{c}.  Note that locale and
+  class definitions allow to include the \indexref{}{keyword}{begin}\mbox{\isa{\isakeyword{begin}}}
+  keyword as well, in order to continue the local theory immediately
+  after the initial specification.
+  
+  \item [\mbox{\isa{\isacommand{end}}}] concludes the current local theory and
+  continues the enclosing global theory.  Note that a non-local
+  \mbox{\isa{\isacommand{end}}} has a different meaning: it concludes the theory
+  itself (\secref{sec:begin-thy}).
+  
+  \item [\isa{{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}}] given after any local theory command
+  specifies an immediate target, e.g.\ ``\mbox{\isa{\isacommand{definition}}}~\isa{{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}}'' or ``\mbox{\isa{\isacommand{theorem}}}~\isa{{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}}''.  This works both in a local or
+  global theory context; the current target context will be suspended
+  for this command only.  Note that \isa{{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}} will always
+  produce a global result independently of the current target context.
+
+  \end{descr}
+
+  The exact meaning of results produced within a local theory context
+  depends on the underlying target infrastructure (locale, type class
+  etc.).  The general idea is as follows, considering a context named
+  \isa{c} with parameter \isa{x} and assumption \isa{A{\isacharbrackleft}x{\isacharbrackright}}.
+  
+  Definitions are exported by introducing a global version with
+  additional arguments; a syntactic abbreviation links the long form
+  with the abstract version of the target context.  For example,
+  \isa{a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}} becomes \isa{c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}} at the theory
+  level (for arbitrary \isa{{\isacharquery}x}), together with a local
+  abbreviation \isa{c\ {\isasymequiv}\ c{\isachardot}a\ x} in the target context (for the
+  fixed parameter \isa{x}).
+
+  Theorems are exported by discharging the assumptions and
+  generalizing the parameters of the context.  For example, \isa{a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}} becomes \isa{c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}} (again for arbitrary
+  \isa{{\isacharquery}x}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Locales \label{sec:locale}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locales are named local contexts, consisting of a list of
+  declaration elements that are modeled after the Isar proof context
+  commands (cf.\ \secref{sec:proof-context}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Locale specifications%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{locale}\mbox{\isa{\isacommand{locale}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+    \indexdef{}{command}{print-locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{command}{print-locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{method}{intro-locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
+    \indexdef{}{method}{unfold-locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
+  \end{matharray}
+
+  \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
+  \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
+  \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
+  \begin{rail}
+    'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
+    ;
+    'print\_locale' '!'? localeexpr
+    ;
+    localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
+    ;
+
+    contextexpr: nameref | '(' contextexpr ')' |
+    (contextexpr (name mixfix? +)) | (contextexpr + '+')
+    ;
+    contextelem: fixes | constrains | assumes | defines | notes
+    ;
+    fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
+    ;
+    constrains: 'constrains' (name '::' type + 'and')
+    ;
+    assumes: 'assumes' (thmdecl? props + 'and')
+    ;
+    defines: 'defines' (thmdecl? prop proppat? + 'and')
+    ;
+    notes: 'notes' (thmdef? thmrefs + 'and')
+    ;
+    includes: 'includes' contextexpr
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{\isacommand{locale}}}~\isa{loc\ {\isacharequal}\ import\ {\isacharplus}\ body}] defines a
+  new locale \isa{loc} as a context consisting of a certain view of
+  existing locales (\isa{import}) plus some additional elements
+  (\isa{body}).  Both \isa{import} and \isa{body} are optional;
+  the degenerate form \mbox{\isa{\isacommand{locale}}}~\isa{loc} defines an empty
+  locale, which may still be useful to collect declarations of facts
+  later on.  Type-inference on locale expressions automatically takes
+  care of the most general typing that the combined context elements
+  may acquire.
+
+  The \isa{import} consists of a structured context expression,
+  consisting of references to existing locales, renamed contexts, or
+  merged contexts.  Renaming uses positional notation: \isa{c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n} means that (a prefix of) the fixed
+  parameters of context \isa{c} are named \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
+  position.  Renaming by default deletes concrete syntax, but new
+  syntax may by specified with a mixfix annotation.  An exeption of
+  this rule is the special syntax declared with ``\isa{{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}}'' (see below), which is neither deleted nor can it
+  be changed.  Merging proceeds from left-to-right, suppressing any
+  duplicates stemming from different paths through the import
+  hierarchy.
+
+  The \isa{body} consists of basic context elements, further context
+  expressions may be included as well.
+
+  \begin{descr}
+
+  \item [\mbox{\isa{fixes}}~\isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}}] declares a local
+  parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
+  are optional).  The special syntax declaration ``\isa{{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}}'' means that \isa{x} may be referenced
+  implicitly in this context.
+
+  \item [\mbox{\isa{constrains}}~\isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}] introduces a type
+  constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
+
+  \item [\mbox{\isa{assumes}}~\isa{a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}]
+  introduces local premises, similar to \mbox{\isa{\isacommand{assume}}} within a
+  proof (cf.\ \secref{sec:proof-context}).
+
+  \item [\mbox{\isa{defines}}~\isa{a{\isacharcolon}\ x\ {\isasymequiv}\ t}] defines a previously
+  declared parameter.  This is close to \mbox{\isa{\isacommand{def}}} within a
+  proof (cf.\ \secref{sec:proof-context}), but \mbox{\isa{defines}}
+  takes an equational proposition instead of variable-term pair.  The
+  left-hand side of the equation may have additional arguments, e.g.\
+  ``\mbox{\isa{defines}}~\isa{f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t}''.
+
+  \item [\mbox{\isa{notes}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
+  reconsiders facts within a local context.  Most notably, this may
+  include arbitrary declarations in any attribute specifications
+  included here, e.g.\ a local \mbox{\isa{simp}} rule.
+
+  \item [\mbox{\isa{includes}}~\isa{c}] copies the specified context
+  in a statically scoped manner.  Only available in the long goal
+  format of \secref{sec:goals}.
+
+  In contrast, the initial \isa{import} specification of a locale
+  expression maintains a dynamic relation to the locales being
+  referenced (benefiting from any later fact declarations in the
+  obvious manner).
+
+  \end{descr}
+  
+  Note that ``\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}'' patterns given
+  in the syntax of \mbox{\isa{assumes}} and \mbox{\isa{defines}} above
+  are illegal in locale definitions.  In the long goal format of
+  \secref{sec:goals}, term bindings may be included as expected,
+  though.
+  
+  \medskip By default, locale specifications are ``closed up'' by
+  turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
+  (modulo local definitions).  The predicate statement covers only the
+  newly specified assumptions, omitting the content of included locale
+  expressions.  The full cumulative view is only provided on export,
+  involving another predicate \isa{loc} that refers to the complete
+  specification text.
+  
+  In any case, the predicate arguments are those locale parameters
+  that actually occur in the respective piece of text.  Also note that
+  these predicates operate at the meta-level in theory, but the locale
+  packages attempts to internalize statements according to the
+  object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
+  \isa{{\isasymLongrightarrow}} by \isa{{\isasymlongrightarrow}} in HOL; see also
+  \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
+  
+  The \isa{{\isacharparenleft}open{\isacharparenright}} option of a locale specification prevents both
+  the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
+  constructions.  Predicates are also omitted for empty specification
+  texts.
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{import\ {\isacharplus}\ body}] prints the
+  specified locale expression in a flattened form.  The notable
+  special case \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{loc} just prints the
+  contents of the named locale, but keep in mind that type-inference
+  will normalize type variables according to the usual alphabetical
+  order.  The command omits \mbox{\isa{notes}} elements by default.
+  Use \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isacharbang}} to get them included.
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}] prints the names of all locales
+  of the current theory.
+
+  \item [\mbox{\isa{intro{\isacharunderscore}locales}} and \mbox{\isa{unfold{\isacharunderscore}locales}}]
+  repeatedly expand all introduction rules of locale predicates of the
+  theory.  While \mbox{\isa{intro{\isacharunderscore}locales}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
+  assumptions, \mbox{\isa{unfold{\isacharunderscore}locales}} is more aggressive and applies
+  \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale
+  specifications entailed by the context, both from target and
+  \mbox{\isa{includes}} statements, and from interpretations (see
+  below).  New goals that are entailed by the current context are
+  discharged automatically.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Interpretation of locales%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locale expressions (more precisely, \emph{context expressions}) may
+  be instantiated, and the instantiated facts added to the current
+  context.  This requires a proof of the instantiated specification
+  and is called \emph{locale interpretation}.  Interpretation is
+  possible in theories and locales (command \mbox{\isa{\isacommand{interpretation}}}) and also within a proof body (\mbox{\isa{\isacommand{interpret}}}).
+
+  \begin{matharray}{rcl}
+    \indexdef{}{command}{interpretation}\mbox{\isa{\isacommand{interpretation}}} & : & \isartrans{theory}{proof(prove)} \\
+    \indexdef{}{command}{interpret}\mbox{\isa{\isacommand{interpret}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+    \indexdef{}{command}{print-interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{\isactrlsup {\isacharasterisk}} & : &  \isarkeep{theory~|~proof} \\
+  \end{matharray}
+
+  \indexouternonterm{interp}
+  \begin{rail}
+    'interpretation' (interp | name ('<' | subseteq) contextexpr)
+    ;
+    'interpret' interp
+    ;
+    'print\_interps' '!'? name
+    ;
+    instantiation: ('[' (inst+) ']')?
+    ;
+    interp: thmdecl? \\ (contextexpr instantiation |
+      name instantiation 'where' (thmdecl? prop + 'and'))
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{interpretation}}}~\isa{expr\ insts\ {\isasymWHERE}\ eqns}]
+
+  The first form of \mbox{\isa{\isacommand{interpretation}}} interprets \isa{expr} in the theory.  The instantiation is given as a list of terms
+  \isa{insts} and is positional.  All parameters must receive an
+  instantiation term --- with the exception of defined parameters.
+  These are, if omitted, derived from the defining equation and other
+  instantiations.  Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
+  Free variables are automatically generalized.
+
+  The command generates proof obligations for the instantiated
+  specifications (assumes and defines elements).  Once these are
+  discharged by the user, instantiated facts are added to the theory
+  in a post-processing phase.
+
+  Additional equations, which are unfolded in facts during
+  post-processing, may be given after the keyword \mbox{\isa{\isakeyword{where}}}.
+  This is useful for interpreting concepts introduced through
+  definition specification elements.  The equations must be proved.
+  Note that if equations are present, the context expression is
+  restricted to a locale name.
+
+  The command is aware of interpretations already active in the
+  theory.  No proof obligations are generated for those, neither is
+  post-processing applied to their facts.  This avoids duplication of
+  interpreted facts, in particular.  Note that, in the case of a
+  locale with import, parts of the interpretation may already be
+  active.  The command will only generate proof obligations and
+  process facts for new parts.
+
+  The context expression may be preceded by a name and/or attributes.
+  These take effect in the post-processing of facts.  The name is used
+  to prefix fact names, for example to avoid accidental hiding of
+  other facts.  Attributes are applied after attributes of the
+  interpreted facts.
+
+  Adding facts to locales has the effect of adding interpreted facts
+  to the theory for all active interpretations also.  That is,
+  interpretations dynamically participate in any facts added to
+  locales.
+
+  \item [\mbox{\isa{\isacommand{interpretation}}}~\isa{name\ {\isasymsubseteq}\ expr}]
+
+  This form of the command interprets \isa{expr} in the locale
+  \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the
+  localized version of the theorem command, the proof is in the
+  context of \isa{name}.  After the proof obligation has been
+  dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
+  context \isa{name} is subsequently entered.  Note that, like
+  import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
+  Like facts of renamed context elements, facts obtained by
+  interpretation may be accessed by prefixing with the parameter
+  renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
+
+  Unlike interpretation in theories, instantiation is confined to the
+  renaming of parameters, which may be specified as part of the
+  context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
+
+  Only specification fragments of \isa{expr} that are not already
+  part of \isa{name} (be it imported, derived or a derived fragment
+  of the import) are considered by interpretation.  This enables
+  circular interpretations.
+
+  If interpretations of \isa{name} exist in the current theory, the
+  command adds interpretations for \isa{expr} as well, with the same
+  prefix and attributes, although only for fragments of \isa{expr}
+  that are not interpreted in the theory already.
+
+  \item [\mbox{\isa{\isacommand{interpret}}}~\isa{expr\ insts\ {\isasymWHERE}\ eqns}]
+  interprets \isa{expr} in the proof context and is otherwise
+  similar to interpretation in theories.  Free variables in
+  instantiations are not generalized, however.
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}~\isa{loc}] prints the
+  interpretations of a particular locale \isa{loc} that are active
+  in the current context, either theory or proof context.  The
+  exclamation point argument triggers printing of \emph{witness}
+  theorems justifying interpretations.  These are normally omitted
+  from the output.
+  
+  \end{descr}
+
+  \begin{warn}
+    Since attributes are applied to interpreted theorems,
+    interpretation may modify the context of common proof tools, e.g.\
+    the Simplifier or Classical Reasoner.  Since the behavior of such
+    automated reasoning tools is \emph{not} stable under
+    interpretation morphisms, manual declarations might have to be
+    issued.
+  \end{warn}
+
+  \begin{warn}
+    An interpretation in a theory may subsume previous
+    interpretations.  This happens if the same specification fragment
+    is interpreted twice and the instantiation of the second
+    interpretation is more general than the interpretation of the
+    first.  A warning is issued, since it is likely that these could
+    have been generalized in the first place.  The locale package does
+    not attempt to remove subsumed interpretations.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Classes \label{sec:class}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A class is a particular locale with \emph{exactly one} type variable
+  \isa{{\isasymalpha}}.  Beyond the underlying locale, a corresponding type class
+  is established which is interpreted logically as axiomatic type
+  class \cite{Wenzel:1997:TPHOL} whose logical content are the
+  assumptions of the locale.  Thus, classes provide the full
+  generality of locales combined with the commodity of type classes
+  (notably type-inference).  See \cite{isabelle-classes} for a short
+  tutorial.
+
+  \begin{matharray}{rcl}
+    \indexdef{}{command}{class}\mbox{\isa{\isacommand{class}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+    \indexdef{}{command}{instantiation}\mbox{\isa{\isacommand{instantiation}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+    \indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
+    \indexdef{}{command}{subclass}\mbox{\isa{\isacommand{subclass}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
+    \indexdef{}{command}{print-classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{method}{intro-classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
+  \end{matharray}
+
+  \begin{rail}
+    'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
+      'begin'?
+    ;
+    'instantiation' (nameref + 'and') '::' arity 'begin'
+    ;
+    'instance'
+    ;
+    'subclass' target? nameref
+    ;
+    'print\_classes'
+    ;
+
+    superclassexpr: nameref | (nameref '+' superclassexpr)
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{class}}}~\isa{c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body}] defines
+  a new class \isa{c}, inheriting from \isa{superclasses}.  This
+  introduces a locale \isa{c} with import of all locales \isa{superclasses}.
+
+  Any \mbox{\isa{fixes}} in \isa{body} are lifted to the global
+  theory level (\emph{class operations} \isa{f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n} of class \isa{c}), mapping the local type parameter
+  \isa{{\isasymalpha}} to a schematic type variable \isa{{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c}.
+
+  Likewise, \mbox{\isa{assumes}} in \isa{body} are also lifted,
+  mapping each local parameter \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} to its
+  corresponding global constant \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}}.  The
+  corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}.  This rule should be rarely needed directly
+  --- the \mbox{\isa{intro{\isacharunderscore}classes}} method takes care of the details of
+  class membership proofs.
+
+  \item [\mbox{\isa{\isacommand{instantiation}}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}}] opens a theory target (cf.\
+  \secref{sec:target}) which allows to specify class operations \isa{f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n} corresponding to sort \isa{s} at the
+  particular type instance \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t}.  An plain \mbox{\isa{\isacommand{instance}}} command
+  in the target body poses a goal stating these type arities.  The
+  target is concluded by an \indexref{}{command}{end}\mbox{\isa{\isacommand{end}}} command.
+
+  Note that a list of simultaneous type constructors may be given;
+  this corresponds nicely to mutual recursive type definitions, e.g.\
+  in Isabelle/HOL.
+
+  \item [\mbox{\isa{\isacommand{instance}}}] in an instantiation target body sets
+  up a goal stating the type arities claimed at the opening \mbox{\isa{\isacommand{instantiation}}}.  The proof would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish the characteristic theorems of
+  the type classes involved.  After finishing the proof, the
+  background theory will be augmented by the proven type arities.
+
+  \item [\mbox{\isa{\isacommand{subclass}}}~\isa{c}] in a class context for class
+  \isa{d} sets up a goal stating that class \isa{c} is logically
+  contained in class \isa{d}.  After finishing the proof, class
+  \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}] prints all classes in the current
+  theory.
+
+  \item [\mbox{\isa{intro{\isacharunderscore}classes}}] repeatedly expands all class
+  introduction rules of this theory.  Note that this method usually
+  needs not be named explicitly, as it is already included in the
+  default proof step (e.g.\ of \mbox{\isa{\isacommand{proof}}}).  In particular,
+  instantiation of trivial (syntactic) classes may be performed by a
+  single ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' proof step.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The class target%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+%FIXME check
+
+  A named context may refer to a locale (cf.\ \secref{sec:target}).
+  If this locale is also a class \isa{c}, apart from the common
+  locale target behaviour the following happens.
+
+  \begin{itemize}
+
+  \item Local constant declarations \isa{g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} referring to the
+  local type parameter \isa{{\isasymalpha}} and local parameters \isa{f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}
+  are accompanied by theory-level constants \isa{g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}}
+  referring to theory-level class operations \isa{f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}}.
+
+  \item Local theorem bindings are lifted as are assumptions.
+
+  \item Local syntax refers to local operations \isa{g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} and
+  global operations \isa{g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}} uniformly.  Type inference
+  resolves ambiguities.  In rare cases, manual type annotations are
+  needed.
+  
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Axiomatic type classes \label{sec:axclass}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{axclass}\mbox{\isa{\isacommand{axclass}}} & : & \isartrans{theory}{theory} \\
+    \indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{theory}{proof(prove)} \\
+  \end{matharray}
+
+  Axiomatic type classes are Isabelle/Pure's primitive
+  \emph{definitional} interface to type classes.  For practical
+  applications, you should consider using classes
+  (cf.~\secref{sec:classes}) which provide high level interface.
+
+  \begin{rail}
+    'axclass' classdecl (axmdecl prop +)
+    ;
+    'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{\isacommand{axclass}}}~\isa{c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms}] defines an axiomatic type class as the intersection of
+  existing classes, with additional axioms holding.  Class axioms may
+  not contain more than one type variable.  The class axioms (with
+  implicit sort constraints added) are bound to the given names.
+  Furthermore a class introduction rule is generated (being bound as
+  \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \mbox{\isa{intro{\isacharunderscore}classes}} to support instantiation proofs of this class.
+  
+  The ``class axioms'' are stored as theorems according to the given
+  name specifications, adding \isa{c{\isacharunderscore}class} as name space prefix;
+  the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
+  
+  \item [\mbox{\isa{\isacommand{instance}}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}} and
+  \mbox{\isa{\isacommand{instance}}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s}]
+  setup a goal stating a class relation or type arity.  The proof
+  would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish
+  the characteristic theorems of the type classes involved.  After
+  finishing the proof, the theory will be augmented by a type
+  signature declaration corresponding to the resulting theorem.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Arbitrary overloading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/Pure's definitional schemes support certain forms of
+  overloading (see \secref{sec:consts}).  At most occassions
+  overloading will be used in a Haskell-like fashion together with
+  type classes by means of \mbox{\isa{\isacommand{instantiation}}} (see
+  \secref{sec:class}).  Sometimes low-level overloading is desirable.
+  The \mbox{\isa{\isacommand{overloading}}} target provides a convenient view for
+  end-users.
+
+  \begin{matharray}{rcl}
+    \indexdef{}{command}{overloading}\mbox{\isa{\isacommand{overloading}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+  \end{matharray}
+
+  \begin{rail}
+    'overloading' \\
+    ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{overloading}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n{\isacharbraceright}\ {\isasymBEGIN}}]
+  opens a theory target (cf.\ \secref{sec:target}) which allows to
+  specify constants with overloaded definitions.  These are identified
+  by an explicitly given mapping from variable names \isa{x\isactrlsub i} to constants \isa{c\isactrlsub i} at particular type
+  instances.  The definitions themselves are established using common
+  specification tools, using the names \isa{x\isactrlsub i} as
+  reference to the corresponding constants.  The target is concluded
+  by \mbox{\isa{\isacommand{end}}}.
+
+  A \isa{{\isacharparenleft}unchecked{\isacharparenright}} option disables global dependency checks for
+  the corresponding definition, which is occasionally useful for
+  exotic overloading.  It is at the discretion of the user to avoid
+  malformed theory specifications!
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Configuration options%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/Pure maintains a record of named configuration options
+  within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|.  Tools may declare
+  options in ML, and then refer to these values (relative to the
+  context).  Thus global reference variables are easily avoided.  The
+  user may change the value of a configuration option by means of an
+  associated attribute of the same name.  This form of context
+  declaration works particularly well with commands such as \mbox{\isa{\isacommand{declare}}} or \mbox{\isa{\isacommand{using}}}.
+
+  For historical reasons, some tools cannot take the full proof
+  context into account and merely refer to the background theory.
+  This is accommodated by configuration options being declared as
+  ``global'', which may not be changed within a local context.
+
+  \begin{matharray}{rcll}
+    \indexdef{}{command}{print-configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
+  \end{matharray}
+
+  \begin{rail}
+    name ('=' ('true' | 'false' | int | name))?
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}] prints the available
+  configuration options, with names, types, and current values.
+  
+  \item [\isa{name\ {\isacharequal}\ value}] as an attribute expression modifies
+  the named option, with the syntax of the value depending on the
+  option's type.  For \verb|bool| the default value is \isa{true}.  Any attempt to change a global option in a local context is
+  ignored.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Derived proof schemes%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Generalized elimination \label{sec:obtain}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{obtain}\mbox{\isa{\isacommand{obtain}}} & : & \isartrans{proof(state)}{proof(prove)} \\
+    \indexdef{}{command}{guess}\mbox{\isa{\isacommand{guess}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isartrans{proof(state)}{proof(prove)} \\
+  \end{matharray}
+
+  Generalized elimination means that additional elements with certain
+  properties may be introduced in the current context, by virtue of a
+  locally proven ``soundness statement''.  Technically speaking, the
+  \mbox{\isa{\isacommand{obtain}}} language element is like a declaration of
+  \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} (see also see
+  \secref{sec:proof-context}), together with a soundness proof of its
+  additional claim.  According to the nature of existential reasoning,
+  assumptions get eliminated from any result exported from the context
+  later, provided that the corresponding parameters do \emph{not}
+  occur in the conclusion.
+
+  \begin{rail}
+    'obtain' parname? (vars + 'and') 'where' (props + 'and')
+    ;
+    'guess' (vars + 'and')
+    ;
+  \end{rail}
+
+  The derived Isar command \mbox{\isa{\isacommand{obtain}}} is defined as follows
+  (where \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k} shall refer to (optional)
+  facts indicated for forward chaining).
+  \begin{matharray}{l}
+    \isa{{\isasymlangle}facts\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}} \\
+    \mbox{\isa{\isacommand{obtain}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}} \\[1ex]
+    \quad \mbox{\isa{\isacommand{have}}}~\isa{{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis} \\
+    \quad \mbox{\isa{\isacommand{proof}}}~\isa{succeed} \\
+    \qquad \mbox{\isa{\isacommand{fix}}}~\isa{thesis} \\
+    \qquad \mbox{\isa{\isacommand{assume}}}~\isa{that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis} \\
+    \qquad \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}~\isa{thesis} \\
+    \quad\qquad \mbox{\isa{\isacommand{apply}}}~\isa{{\isacharminus}} \\
+    \quad\qquad \mbox{\isa{\isacommand{using}}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}} \\
+    \quad \mbox{\isa{\isacommand{qed}}} \\
+    \quad \mbox{\isa{\isacommand{fix}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}~\mbox{\isa{\isacommand{assume}}}\isa{\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n} \\
+  \end{matharray}
+
+  Typically, the soundness proof is relatively straight-forward, often
+  just by canonical automated tools such as ``\mbox{\isa{\isacommand{by}}}~\isa{simp}'' or ``\mbox{\isa{\isacommand{by}}}~\isa{blast}''.  Accordingly, the
+  ``\isa{that}'' reduction above is declared as simplification and
+  introduction rule.
+
+  In a sense, \mbox{\isa{\isacommand{obtain}}} represents at the level of Isar
+  proofs what would be meta-logical existential quantifiers and
+  conjunctions.  This concept has a broad range of useful
+  applications, ranging from plain elimination (or introduction) of
+  object-level existential and conjunctions, to elimination over
+  results of symbolic evaluation of recursive definitions, for
+  example.  Also note that \mbox{\isa{\isacommand{obtain}}} without parameters acts
+  much like \mbox{\isa{\isacommand{have}}}, where the result is treated as a
+  genuine assumption.
+
+  An alternative name to be used instead of ``\isa{that}'' above may
+  be given in parentheses.
+
+  \medskip The improper variant \mbox{\isa{\isacommand{guess}}} is similar to
+  \mbox{\isa{\isacommand{obtain}}}, but derives the obtained statement from the
+  course of reasoning!  The proof starts with a fixed goal \isa{thesis}.  The subsequent proof may refine this to anything of the
+  form like \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis}, but must not introduce new subgoals.  The
+  final goal state is then used as reduction rule for the obtain
+  scheme described above.  Obtained parameters \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m} are marked as internal by default, which prevents the
+  proof context from being polluted by ad-hoc variables.  The variable
+  names and type constraints given as arguments for \mbox{\isa{\isacommand{guess}}}
+  specify a prefix of obtained parameters explicitly in the text.
+
+  It is important to note that the facts introduced by \mbox{\isa{\isacommand{obtain}}} and \mbox{\isa{\isacommand{guess}}} may not be polymorphic: any
+  type-variables occurring here are fixed in the present context!%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Calculational reasoning \label{sec:calculation}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{also}\mbox{\isa{\isacommand{also}}} & : & \isartrans{proof(state)}{proof(state)} \\
+    \indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
+    \indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
+    \indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
+    \indexdef{}{command}{print-trans-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \mbox{\isa{trans}} & : & \isaratt \\
+    \mbox{\isa{sym}} & : & \isaratt \\
+    \mbox{\isa{symmetric}} & : & \isaratt \\
+  \end{matharray}
+
+  Calculational proof is forward reasoning with implicit application
+  of transitivity rules (such those of \isa{{\isacharequal}}, \isa{{\isasymle}},
+  \isa{{\isacharless}}).  Isabelle/Isar maintains an auxiliary fact register
+  \indexref{}{fact}{calculation}\mbox{\isa{calculation}} for accumulating results obtained by
+  transitivity composed with the current result.  Command \mbox{\isa{\isacommand{also}}} updates \mbox{\isa{calculation}} involving \mbox{\isa{this}}, while
+  \mbox{\isa{\isacommand{finally}}} exhibits the final \mbox{\isa{calculation}} by
+  forward chaining towards the next goal statement.  Both commands
+  require valid current facts, i.e.\ may occur only after commands
+  that produce theorems such as \mbox{\isa{\isacommand{assume}}}, \mbox{\isa{\isacommand{note}}}, or some finished proof of \mbox{\isa{\isacommand{have}}}, \mbox{\isa{\isacommand{show}}} etc.  The \mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}
+  commands are similar to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}},
+  but only collect further results in \mbox{\isa{calculation}} without
+  applying any rules yet.
+
+  Also note that the implicit term abbreviation ``\isa{{\isasymdots}}'' has
+  its canonical application with calculational proofs.  It refers to
+  the argument of the preceding statement. (The argument of a curried
+  infix expression happens to be its right-hand side.)
+
+  Isabelle/Isar calculations are implicitly subject to block structure
+  in the sense that new threads of calculational reasoning are
+  commenced for any new block (as opened by a local goal, for
+  example).  This means that, apart from being able to nest
+  calculations, there is no separate \emph{begin-calculation} command
+  required.
+
+  \medskip The Isar calculation proof commands may be defined as
+  follows:\footnote{We suppress internal bookkeeping such as proper
+  handling of block-structure.}
+
+  \begin{matharray}{rcl}
+    \mbox{\isa{\isacommand{also}}}\isa{\isactrlsub {\isadigit{0}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ this} \\
+    \mbox{\isa{\isacommand{also}}}\isa{\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}} \\[0.5ex]
+    \mbox{\isa{\isacommand{finally}}} & \equiv & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
+    \mbox{\isa{\isacommand{moreover}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ calculation\ this} \\
+    \mbox{\isa{\isacommand{ultimately}}} & \equiv & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\
+  \end{matharray}
+
+  \begin{rail}
+    ('also' | 'finally') ('(' thmrefs ')')?
+    ;
+    'trans' (() | 'add' | 'del')
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{also}}}~\isa{{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}}]
+  maintains the auxiliary \mbox{\isa{calculation}} register as follows.
+  The first occurrence of \mbox{\isa{\isacommand{also}}} in some calculational
+  thread initializes \mbox{\isa{calculation}} by \mbox{\isa{this}}. Any
+  subsequent \mbox{\isa{\isacommand{also}}} on the same level of block-structure
+  updates \mbox{\isa{calculation}} by some transitivity rule applied to
+  \mbox{\isa{calculation}} and \mbox{\isa{this}} (in that order).  Transitivity
+  rules are picked from the current context, unless alternative rules
+  are given as explicit arguments.
+
+  \item [\mbox{\isa{\isacommand{finally}}}~\isa{{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}}]
+  maintaining \mbox{\isa{calculation}} in the same way as \mbox{\isa{\isacommand{also}}}, and concludes the current calculational thread.  The final
+  result is exhibited as fact for forward chaining towards the next
+  goal. Basically, \mbox{\isa{\isacommand{finally}}} just abbreviates \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\mbox{\isa{calculation}}.  Typical idioms for
+  concluding calculational proofs are ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{show}}}~\isa{{\isacharquery}thesis}~\mbox{\isa{\isacommand{{\isachardot}}}}'' and ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{{\isachardot}}}}''.
+
+  \item [\mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}] are
+  analogous to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}}, but collect
+  results only, without applying rules.
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}] prints the list of
+  transitivity rules (for calculational commands \mbox{\isa{\isacommand{also}}} and
+  \mbox{\isa{\isacommand{finally}}}) and symmetry rules (for the \mbox{\isa{symmetric}} operation and single step elimination patters) of the
+  current context.
+
+  \item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
+
+  \item [\mbox{\isa{sym}}] declares symmetry rules, as well as
+  \mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
+
+  \item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
+  declared as \mbox{\isa{sym}} in the current context.  For example,
+  ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y}'' produces a
+  swapped fact derived from that assumption.
+
+  In structured proof texts it is often more appropriate to use an
+  explicit single-step elimination proof, such as ``\mbox{\isa{\isacommand{assume}}}~\isa{x\ {\isacharequal}\ y}~\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}~\isa{y\ {\isacharequal}\ x}~\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof tools%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Miscellaneous methods and attributes \label{sec:misc-meth-att}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{unfold}\mbox{\isa{unfold}} & : & \isarmeth \\
+    \indexdef{}{method}{fold}\mbox{\isa{fold}} & : & \isarmeth \\
+    \indexdef{}{method}{insert}\mbox{\isa{insert}} & : & \isarmeth \\[0.5ex]
+    \indexdef{}{method}{erule}\mbox{\isa{erule}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{drule}\mbox{\isa{drule}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{frule}\mbox{\isa{frule}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{succeed}\mbox{\isa{succeed}} & : & \isarmeth \\
+    \indexdef{}{method}{fail}\mbox{\isa{fail}} & : & \isarmeth \\
+  \end{matharray}
+
+  \begin{rail}
+    ('fold' | 'unfold' | 'insert') thmrefs
+    ;
+    ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{unfold}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n} and \mbox{\isa{fold}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] expand (or fold back) the
+  given definitions throughout all goals; any chained facts provided
+  are inserted into the goal and subject to rewriting as well.
+
+  \item [\mbox{\isa{insert}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] inserts
+  theorems as facts into all goals of the proof state.  Note that
+  current facts indicated for forward chaining are ignored.
+
+  \item [\mbox{\isa{erule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}, \mbox{\isa{drule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}, and \mbox{\isa{frule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] are similar to the basic \mbox{\isa{rule}}
+  method (see \secref{sec:pure-meth-att}), but apply rules by
+  elim-resolution, destruct-resolution, and forward-resolution,
+  respectively \cite{isabelle-ref}.  The optional natural number
+  argument (default 0) specifies additional assumption steps to be
+  performed here.
+
+  Note that these methods are improper ones, mainly serving for
+  experimentation and tactic script emulation.  Different modes of
+  basic rule application are usually expressed in Isar at the proof
+  language level, rather than via implicit proof state manipulations.
+  For example, a proper single-step elimination would be done using
+  the plain \mbox{\isa{rule}} method, with forward chaining of current
+  facts.
+
+  \item [\mbox{\isa{succeed}}] yields a single (unchanged) result; it is
+  the identity of the ``\isa{{\isacharcomma}}'' method combinator (cf.\
+  \secref{sec:syn-meth}).
+
+  \item [\mbox{\isa{fail}}] yields an empty result sequence; it is the
+  identity of the ``\isa{{\isacharbar}}'' method combinator (cf.\
+  \secref{sec:syn-meth}).
+
+  \end{descr}
+
+  \begin{matharray}{rcl}
+    \indexdef{}{attribute}{tagged}\mbox{\isa{tagged}} & : & \isaratt \\
+    \indexdef{}{attribute}{untagged}\mbox{\isa{untagged}} & : & \isaratt \\[0.5ex]
+    \indexdef{}{attribute}{THEN}\mbox{\isa{THEN}} & : & \isaratt \\
+    \indexdef{}{attribute}{COMP}\mbox{\isa{COMP}} & : & \isaratt \\[0.5ex]
+    \indexdef{}{attribute}{unfolded}\mbox{\isa{unfolded}} & : & \isaratt \\
+    \indexdef{}{attribute}{folded}\mbox{\isa{folded}} & : & \isaratt \\[0.5ex]
+    \indexdef{}{attribute}{rotated}\mbox{\isa{rotated}} & : & \isaratt \\
+    \indexdef{Pure}{attribute}{elim-format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
+    \indexdef{}{attribute}{standard}\mbox{\isa{standard}}\isa{\isactrlsup {\isacharasterisk}} & : & \isaratt \\
+    \indexdef{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{\isactrlsup {\isacharasterisk}} & : & \isaratt \\
+  \end{matharray}
+
+  \begin{rail}
+    'tagged' nameref
+    ;
+    'untagged' name
+    ;
+    ('THEN' | 'COMP') ('[' nat ']')? thmref
+    ;
+    ('unfolded' | 'folded') thmrefs
+    ;
+    'rotated' ( int )?
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{tagged}}~\isa{name\ arg} and \mbox{\isa{untagged}}~\isa{name}] add and remove \emph{tags} of some theorem.
+  Tags may be any list of string pairs that serve as formal comment.
+  The first string is considered the tag name, the second its
+  argument.  Note that \mbox{\isa{untagged}} removes any tags of the
+  same name.
+
+  \item [\mbox{\isa{THEN}}~\isa{a} and \mbox{\isa{COMP}}~\isa{a}]
+  compose rules by resolution.  \mbox{\isa{THEN}} resolves with the
+  first premise of \isa{a} (an alternative position may be also
+  specified); the \mbox{\isa{COMP}} version skips the automatic
+  lifting process that is normally intended (cf.\ \verb|op RS| and
+  \verb|op COMP| in \cite[\S5]{isabelle-ref}).
+  
+  \item [\mbox{\isa{unfolded}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n} and
+  \mbox{\isa{folded}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] expand and fold
+  back again the given definitions throughout a rule.
+
+  \item [\mbox{\isa{rotated}}~\isa{n}] rotate the premises of a
+  theorem by \isa{n} (default 1).
+
+  \item [\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}] turns a destruction rule into
+  elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
+  
+  Note that the Classical Reasoner (\secref{sec:classical}) provides
+  its own version of this operation.
+
+  \item [\mbox{\isa{standard}}] puts a theorem into the standard form
+  of object-rules at the outermost theory level.  Note that this
+  operation violates the local proof context (including active
+  locales).
+
+  \item [\mbox{\isa{no{\isacharunderscore}vars}}] replaces schematic variables by free
+  ones; this is mainly for tuning output of pretty printed theorems.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The following improper proof methods emulate traditional tactics.
+  These admit direct access to the goal state, which is normally
+  considered harmful!  In particular, this may involve both numbered
+  goal addressing (default 1), and dynamic instantiation within the
+  scope of some subgoal.
+
+  \begin{warn}
+    Dynamic instantiations refer to universally quantified parameters
+    of a subgoal (the dynamic context) rather than fixed variables and
+    term abbreviations of a (static) Isar context.
+  \end{warn}
+
+  Tactic emulation methods, unlike their ML counterparts, admit
+  simultaneous instantiation from both dynamic and static contexts.
+  If names occur in both contexts goal parameters hide locally fixed
+  variables.  Likewise, schematic variables refer to term
+  abbreviations, if present in the static context.  Otherwise the
+  schematic variable is interpreted as a schematic variable and left
+  to be solved by unification with certain parts of the subgoal.
+
+  Note that the tactic emulation proof methods in Isabelle/Isar are
+  consistently named \isa{foo{\isacharunderscore}tac}.  Note also that variable names
+  occurring on left hand sides of instantiations must be preceded by a
+  question mark if they coincide with a keyword or contain dots.  This
+  is consistent with the attribute \mbox{\isa{where}} (see
+  \secref{sec:pure-meth-att}).
+
+  \begin{matharray}{rcl}
+    \indexdef{}{method}{rule-tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{erule-tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{drule-tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{frule-tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{cut-tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{thin-tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{subgoal-tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{rename-tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{rotate-tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{tactic}\mbox{\isa{tactic}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+  \end{matharray}
+
+  \begin{rail}
+    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
+    ( insts thmref | thmrefs )
+    ;
+    'subgoal\_tac' goalspec? (prop +)
+    ;
+    'rename\_tac' goalspec? (name +)
+    ;
+    'rotate\_tac' goalspec? int?
+    ;
+    'tactic' text
+    ;
+
+    insts: ((name '=' term) + 'and') 'in'
+    ;
+  \end{rail}
+
+\begin{descr}
+
+  \item [\mbox{\isa{rule{\isacharunderscore}tac}} etc.] do resolution of rules with explicit
+  instantiation.  This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}).
+
+  Multiple rules may be only given if there is no instantiation; then
+  \mbox{\isa{rule{\isacharunderscore}tac}} is the same as \verb|resolve_tac| in ML (see
+  \cite[\S3]{isabelle-ref}).
+
+  \item [\mbox{\isa{cut{\isacharunderscore}tac}}] inserts facts into the proof state as
+  assumption of a subgoal, see also \verb|cut_facts_tac| in
+  \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
+  variables is spread over the main goal statement.  Instantiations
+  may be given as well, see also ML tactic \verb|cut_inst_tac| in
+  \cite[\S3]{isabelle-ref}.
+
+  \item [\mbox{\isa{thin{\isacharunderscore}tac}}~\isa{{\isasymphi}}] deletes the specified
+  assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic
+  variables.  See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
+
+  \item [\mbox{\isa{subgoal{\isacharunderscore}tac}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an
+  assumption to a subgoal.  See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
+
+  \item [\mbox{\isa{rename{\isacharunderscore}tac}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n}] renames
+  parameters of a goal according to the list \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n}, which refers to the \emph{suffix} of variables.
+
+  \item [\mbox{\isa{rotate{\isacharunderscore}tac}}~\isa{n}] rotates the assumptions of a
+  goal by \isa{n} positions: from right to left if \isa{n} is
+  positive, and from left to right if \isa{n} is negative; the
+  default value is 1.  See also \verb|rotate_tac| in
+  \cite[\S3]{isabelle-ref}.
+
+  \item [\mbox{\isa{tactic}}~\isa{text}] produces a proof method from
+  any ML text of type \verb|tactic|.  Apart from the usual ML
+  environment and the current implicit theory context, the ML code may
+  refer to the following locally bound values:
+
+%FIXME check
+{\footnotesize\begin{verbatim}
+val ctxt  : Proof.context
+val facts : thm list
+val thm   : string -> thm
+val thms  : string -> thm list
+\end{verbatim}}
+
+  Here \verb|ctxt| refers to the current proof context, \verb|facts| indicates any current facts for forward-chaining, and \verb|thm|~/~\verb|thms| retrieve named facts (including global theorems)
+  from the context.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The Simplifier \label{sec:simplifier}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Simplification methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{simp}\mbox{\isa{simp}} & : & \isarmeth \\
+    \indexdef{}{method}{simp-all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
+  \end{matharray}
+
+  \indexouternonterm{simpmod}
+  \begin{rail}
+    ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
+    ;
+
+    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
+    ;
+    simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
+      'split' (() | 'add' | 'del')) ':' thmrefs
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{simp}}] invokes the Simplifier, after declaring
+  additional rules according to the arguments given.  Note that the
+  \railtterm{only} modifier first removes all other rewrite rules,
+  congruences, and looper tactics (including splits), and then behaves
+  like \railtterm{add}.
+
+  \medskip The \railtterm{cong} modifiers add or delete Simplifier
+  congruence rules (see also \cite{isabelle-ref}), the default is to
+  add.
+
+  \medskip The \railtterm{split} modifiers add or delete rules for the
+  Splitter (see also \cite{isabelle-ref}), the default is to add.
+  This works only if the Simplifier method has been properly setup to
+  include the Splitter (all major object logics such HOL, HOLCF, FOL,
+  ZF do this already).
+
+  \item [\mbox{\isa{simp{\isacharunderscore}all}}] is similar to \mbox{\isa{simp}}, but acts on
+  all goals (backwards from the last to the first one).
+
+  \end{descr}
+
+  By default the Simplifier methods take local assumptions fully into
+  account, using equational assumptions in the subsequent
+  normalization process, or simplifying assumptions themselves (cf.\
+  \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}).  In
+  structured proofs this is usually quite well behaved in practice:
+  just the local premises of the actual goal are involved, additional
+  facts may be inserted via explicit forward-chaining (via \mbox{\isa{\isacommand{then}}}, \mbox{\isa{\isacommand{from}}}, \mbox{\isa{\isacommand{using}}} etc.).  The full
+  context of premises is only included if the ``\isa{{\isacharbang}}'' (bang)
+  argument is given, which should be used with some care, though.
+
+  Additional Simplifier options may be specified to tune the behavior
+  further (mostly for unstructured scripts with many accidental local
+  facts): ``\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}'' means assumptions are ignored
+  completely (cf.\ \verb|simp_tac|), ``\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}'' means
+  assumptions are used in the simplification of the conclusion but are
+  not themselves simplified (cf.\ \verb|asm_simp_tac|), and ``\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}'' means assumptions are simplified but are not used
+  in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|).  For compatibility reasons, there is also an option
+  ``\isa{{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}}'', which means that an assumption is only used
+  for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
+
+  Giving an option ``\isa{{\isacharparenleft}depth{\isacharunderscore}limit{\isacharcolon}\ n{\isacharparenright}}'' limits the number of
+  recursive invocations of the simplifier during conditional
+  rewriting.
+
+  \medskip The Splitter package is usually configured to work as part
+  of the Simplifier.  The effect of repeatedly applying \verb|split_tac| can be simulated by ``\isa{{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}}''.  There is also a separate \isa{split}
+  method available for single-step case splitting.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Declaring rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{print-simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{attribute}{simp}\mbox{\isa{simp}} & : & \isaratt \\
+    \indexdef{}{attribute}{cong}\mbox{\isa{cong}} & : & \isaratt \\
+    \indexdef{}{attribute}{split}\mbox{\isa{split}} & : & \isaratt \\
+  \end{matharray}
+
+  \begin{rail}
+    ('simp' | 'cong' | 'split') (() | 'add' | 'del')
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}] prints the collection of rules
+  declared to the Simplifier, which is also known as ``simpset''
+  internally \cite{isabelle-ref}.
+
+  \item [\mbox{\isa{simp}}] declares simplification rules.
+
+  \item [\mbox{\isa{cong}}] declares congruence rules.
+
+  \item [\mbox{\isa{split}}] declares case split rules.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Simplification procedures%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{simproc-setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
+    simproc & : & \isaratt \\
+  \end{matharray}
+
+  \begin{rail}
+    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+    ;
+
+    'simproc' (('add' ':')? | 'del' ':') (name+)
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}] defines a named simplification
+  procedure that is invoked by the Simplifier whenever any of the
+  given term patterns match the current redex.  The implementation,
+  which is provided as ML source text, needs to be of type \verb|morphism -> simpset -> cterm -> thm option|, where the \verb|cterm| represents the current redex \isa{r} and the result is
+  supposed to be some proven rewrite rule \isa{r\ {\isasymequiv}\ r{\isacharprime}} (or a
+  generalized version), or \verb|NONE| to indicate failure.  The
+  \verb|simpset| argument holds the full context of the current
+  Simplifier invocation, including the actual Isar proof context.  The
+  \verb|morphism| informs about the difference of the original
+  compilation context wrt.\ the one of the actual application later
+  on.  The optional \mbox{\isa{\isakeyword{identifier}}} specifies theorems that
+  represent the logical content of the abstract theory of this
+  simproc.
+
+  Morphisms and identifiers are only relevant for simprocs that are
+  defined within a local target context, e.g.\ in a locale.
+
+  \item [\isa{simproc\ add{\isacharcolon}\ name} and \isa{simproc\ del{\isacharcolon}\ name}]
+  add or delete named simprocs to the current Simplifier context.  The
+  default is to add a simproc.  Note that \mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}
+  already adds the new simproc to the subsequent context.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Forward simplification%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{attribute}{simplified}\mbox{\isa{simplified}} & : & \isaratt \\
+  \end{matharray}
+
+  \begin{rail}
+    'simplified' opt? thmrefs?
+    ;
+
+    opt: '(' (noasm | noasmsimp | noasmuse) ')'
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{simplified}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}]
+  causes a theorem to be simplified, either by exactly the specified
+  rules \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n}, or the implicit Simplifier
+  context if no arguments are given.  The result is fully simplified
+  by default, including assumptions and conclusion; the options \isa{no{\isacharunderscore}asm} etc.\ tune the Simplifier in the same way as the for the
+  \isa{simp} method.
+
+  Note that forward simplification restricts the simplifier to its
+  most basic operation of term rewriting; solver and looper tactics
+  \cite{isabelle-ref} are \emph{not} involved here.  The \isa{simplified} attribute should be only rarely required under normal
+  circumstances.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Low-level equational reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{subst}\mbox{\isa{subst}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{hypsubst}\mbox{\isa{hypsubst}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+    \indexdef{}{method}{split}\mbox{\isa{split}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
+  \end{matharray}
+
+  \begin{rail}
+    'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
+    ;
+    'split' ('(' 'asm' ')')? thmrefs
+    ;
+  \end{rail}
+
+  These methods provide low-level facilities for equational reasoning
+  that are intended for specialized applications only.  Normally,
+  single step calculations would be performed in a structured text
+  (see also \secref{sec:calculation}), while the Simplifier methods
+  provide the canonical way for automated normalization (see
+  \secref{sec:simplifier}).
+
+  \begin{descr}
+
+  \item [\mbox{\isa{subst}}~\isa{eq}] performs a single substitution
+  step using rule \isa{eq}, which may be either a meta or object
+  equality.
+
+  \item [\mbox{\isa{subst}}~\isa{{\isacharparenleft}asm{\isacharparenright}\ eq}] substitutes in an
+  assumption.
+
+  \item [\mbox{\isa{subst}}~\isa{{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq}] performs several
+  substitutions in the conclusion. The numbers \isa{i} to \isa{j}
+  indicate the positions to substitute at.  Positions are ordered from
+  the top of the term tree moving down from left to right. For
+  example, in \isa{{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}} there are three positions
+  where commutativity of \isa{{\isacharplus}} is applicable: 1 refers to the
+  whole term, 2 to \isa{a\ {\isacharplus}\ b} and 3 to \isa{c\ {\isacharplus}\ d}.
+
+  If the positions in the list \isa{{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}} are non-overlapping
+  (e.g.\ \isa{{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}} in \isa{{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}}) you may
+  assume all substitutions are performed simultaneously.  Otherwise
+  the behaviour of \isa{subst} is not specified.
+
+  \item [\mbox{\isa{subst}}~\isa{{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq}] performs the
+  substitutions in the assumptions.  Positions \isa{{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}}
+  refer to assumption 1, positions \isa{i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}}
+  to assumption 2, and so on.
+
+  \item [\mbox{\isa{hypsubst}}] performs substitution using some
+  assumption; this only works for equations of the form \isa{x\ {\isacharequal}\ t} where \isa{x} is a free or bound variable.
+
+  \item [\mbox{\isa{split}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] performs
+  single-step case splitting using the given rules.  By default,
+  splitting is performed in the conclusion of a goal; the \isa{{\isacharparenleft}asm{\isacharparenright}} option indicates to operate on assumptions instead.
+  
+  Note that the \mbox{\isa{simp}} method already involves repeated
+  application of split rules as declared in the current context.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The Classical Reasoner \label{sec:classical}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Basic methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\
+    \indexdef{}{method}{contradiction}\mbox{\isa{contradiction}} & : & \isarmeth \\
+    \indexdef{}{method}{intro}\mbox{\isa{intro}} & : & \isarmeth \\
+    \indexdef{}{method}{elim}\mbox{\isa{elim}} & : & \isarmeth \\
+  \end{matharray}
+
+  \begin{rail}
+    ('rule' | 'intro' | 'elim') thmrefs?
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{rule}}] as offered by the Classical Reasoner is a
+  refinement over the primitive one (see \secref{sec:pure-meth-att}).
+  Both versions essentially work the same, but the classical version
+  observes the classical rule context in addition to that of
+  Isabelle/Pure.
+
+  Common object logics (HOL, ZF, etc.) declare a rich collection of
+  classical rules (even if these would qualify as intuitionistic
+  ones), but only few declarations to the rule context of
+  Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+  \item [\mbox{\isa{contradiction}}] solves some goal by contradiction,
+  deriving any result from both \isa{{\isasymnot}\ A} and \isa{A}.  Chained
+  facts, which are guaranteed to participate, may appear in either
+  order.
+
+  \item [\mbox{\isa{intro}} and \mbox{\isa{elim}}] repeatedly refine
+  some goal by intro- or elim-resolution, after having inserted any
+  chained facts.  Exactly the rules given as arguments are taken into
+  account; this allows fine-tuned decomposition of a proof problem, in
+  contrast to common automated tools.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Automated methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{blast}\mbox{\isa{blast}} & : & \isarmeth \\
+    \indexdef{}{method}{fast}\mbox{\isa{fast}} & : & \isarmeth \\
+    \indexdef{}{method}{slow}\mbox{\isa{slow}} & : & \isarmeth \\
+    \indexdef{}{method}{best}\mbox{\isa{best}} & : & \isarmeth \\
+    \indexdef{}{method}{safe}\mbox{\isa{safe}} & : & \isarmeth \\
+    \indexdef{}{method}{clarify}\mbox{\isa{clarify}} & : & \isarmeth \\
+  \end{matharray}
+
+  \indexouternonterm{clamod}
+  \begin{rail}
+    'blast' ('!' ?) nat? (clamod *)
+    ;
+    ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
+    ;
+
+    clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{blast}}] refers to the classical tableau prover (see
+  \verb|blast_tac| in \cite[\S11]{isabelle-ref}).  The optional
+  argument specifies a user-supplied search bound (default 20).
+
+  \item [\mbox{\isa{fast}}, \mbox{\isa{slow}}, \mbox{\isa{best}}, \mbox{\isa{safe}}, and \mbox{\isa{clarify}}] refer to the generic classical
+  reasoner.  See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite[\S11]{isabelle-ref} for
+  more information.
+
+  \end{descr}
+
+  Any of the above methods support additional modifiers of the context
+  of classical rules.  Their semantics is analogous to the attributes
+  given before.  Facts provided by forward chaining are inserted into
+  the goal before commencing proof search.  The ``\isa{{\isacharbang}}''~argument causes the full context of assumptions to be
+  included as well.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Combined automated methods \label{sec:clasimp}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{auto}\mbox{\isa{auto}} & : & \isarmeth \\
+    \indexdef{}{method}{force}\mbox{\isa{force}} & : & \isarmeth \\
+    \indexdef{}{method}{clarsimp}\mbox{\isa{clarsimp}} & : & \isarmeth \\
+    \indexdef{}{method}{fastsimp}\mbox{\isa{fastsimp}} & : & \isarmeth \\
+    \indexdef{}{method}{slowsimp}\mbox{\isa{slowsimp}} & : & \isarmeth \\
+    \indexdef{}{method}{bestsimp}\mbox{\isa{bestsimp}} & : & \isarmeth \\
+  \end{matharray}
+
+  \indexouternonterm{clasimpmod}
+  \begin{rail}
+    'auto' '!'? (nat nat)? (clasimpmod *)
+    ;
+    ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
+    ;
+
+    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
+      ('cong' | 'split') (() | 'add' | 'del') |
+      'iff' (((() | 'add') '?'?) | 'del') |
+      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{auto}}, \mbox{\isa{force}}, \mbox{\isa{clarsimp}}, \mbox{\isa{fastsimp}}, \mbox{\isa{slowsimp}}, and \mbox{\isa{bestsimp}}] provide
+  access to Isabelle's combined simplification and classical reasoning
+  tactics.  These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
+  added as wrapper, see \cite[\S11]{isabelle-ref} for more
+  information.  The modifier arguments correspond to those given in
+  \secref{sec:simplifier} and \secref{sec:classical}.  Just note that
+  the ones related to the Simplifier are prefixed by \railtterm{simp}
+  here.
+
+  Facts provided by forward chaining are inserted into the goal before
+  doing the search.  The ``\isa{{\isacharbang}}'' argument causes the full
+  context of assumptions to be included as well.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Declaring rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{print-claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
+    \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
+    \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
+    \indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\
+    \indexdef{}{attribute}{iff}\mbox{\isa{iff}} & : & \isaratt \\
+  \end{matharray}
+
+  \begin{rail}
+    ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
+    ;
+    'rule' 'del'
+    ;
+    'iff' (((() | 'add') '?'?) | 'del')
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}] prints the collection of rules
+  declared to the Classical Reasoner, which is also known as
+  ``claset'' internally \cite{isabelle-ref}.
+  
+  \item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}]
+  declare introduction, elimination, and destruction rules,
+  respectively.  By default, rules are considered as \emph{unsafe}
+  (i.e.\ not applied blindly without backtracking), while ``\isa{{\isacharbang}}'' classifies as \emph{safe}.  Rule declarations marked by
+  ``\isa{{\isacharquery}}'' coincide with those of Isabelle/Pure, cf.\
+  \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
+  of the \mbox{\isa{rule}} method).  The optional natural number
+  specifies an explicit weight argument, which is ignored by automated
+  tools, but determines the search order of single rule steps.
+
+  \item [\mbox{\isa{rule}}~\isa{del}] deletes introduction,
+  elimination, or destruction rules from the context.
+
+  \item [\mbox{\isa{iff}}] declares logical equivalences to the
+  Simplifier and the Classical reasoner at the same time.
+  Non-conditional rules result in a ``safe'' introduction and
+  elimination pair; conditional ones are considered ``unsafe''.  Rules
+  with negative conclusion are automatically inverted (using \isa{{\isasymnot}} elimination internally).
+
+  The ``\isa{{\isacharquery}}'' version of \mbox{\isa{iff}} declares rules to
+  the Isabelle/Pure context only, and omits the Simplifier
+  declaration.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Classical operations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{attribute}{swapped}\mbox{\isa{swapped}} & : & \isaratt \\
+  \end{matharray}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{swapped}}] turns an introduction rule into an
+  elimination, by resolving with the classical swap principle \isa{{\isacharparenleft}{\isasymnot}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ B{\isacharparenright}}.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Proof by cases and induction \label{sec:cases-induct}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Rule contexts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{case}\mbox{\isa{\isacommand{case}}} & : & \isartrans{proof(state)}{proof(state)} \\
+    \indexdef{}{command}{print-cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{proof} \\
+    \indexdef{}{attribute}{case-names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
+    \indexdef{}{attribute}{case-conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
+    \indexdef{}{attribute}{params}\mbox{\isa{params}} & : & \isaratt \\
+    \indexdef{}{attribute}{consumes}\mbox{\isa{consumes}} & : & \isaratt \\
+  \end{matharray}
+
+  The puristic way to build up Isar proof contexts is by explicit
+  language elements like \mbox{\isa{\isacommand{fix}}}, \mbox{\isa{\isacommand{assume}}},
+  \mbox{\isa{\isacommand{let}}} (see \secref{sec:proof-context}).  This is adequate
+  for plain natural deduction, but easily becomes unwieldy in concrete
+  verification tasks, which typically involve big induction rules with
+  several cases.
+
+  The \mbox{\isa{\isacommand{case}}} command provides a shorthand to refer to a
+  local context symbolically: certain proof methods provide an
+  environment of named ``cases'' of the form \isa{c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n}; the effect of
+  ``\mbox{\isa{\isacommand{case}}}\isa{c}'' is then equivalent to ``\mbox{\isa{\isacommand{fix}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}~\mbox{\isa{\isacommand{assume}}}~\isa{c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}''.  Term bindings may be
+  covered as well, notably \mbox{\isa{{\isacharquery}case}} for the main conclusion.
+
+  By default, the ``terminology'' \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m} of
+  a case value is marked as hidden, i.e.\ there is no way to refer to
+  such parameters in the subsequent proof text.  After all, original
+  rule parameters stem from somewhere outside of the current proof
+  text.  By using the explicit form ``\mbox{\isa{\isacommand{case}}}~\isa{{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}}'' instead, the proof author is able to
+  chose local names that fit nicely into the current context.
+
+  \medskip It is important to note that proper use of \mbox{\isa{\isacommand{case}}} does not provide means to peek at the current goal state,
+  which is not directly observable in Isar!  Nonetheless, goal
+  refinement commands do provide named cases \isa{goal\isactrlsub i}
+  for each subgoal \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n} of the resulting goal state.
+  Using this extra feature requires great care, because some bits of
+  the internal tactical machinery intrude the proof text.  In
+  particular, parameter names stemming from the left-over of automated
+  reasoning tools are usually quite unpredictable.
+
+  Under normal circumstances, the text of cases emerge from standard
+  elimination or induction rules, which in turn are derived from
+  previous theory specifications in a canonical way (say from
+  \mbox{\isa{\isacommand{inductive}}} definitions).
+
+  \medskip Proper cases are only available if both the proof method
+  and the rules involved support this.  By using appropriate
+  attributes, case names, conclusions, and parameters may be also
+  declared by hand.  Thus variant versions of rules that have been
+  derived manually become ready to use in advanced case analysis
+  later.
+
+  \begin{rail}
+    'case' (caseref | '(' caseref ((name | underscore) +) ')')
+    ;
+    caseref: nameref attributes?
+    ;
+
+    'case\_names' (name +)
+    ;
+    'case\_conclusion' name (name *)
+    ;
+    'params' ((name *) + 'and')
+    ;
+    'consumes' nat?
+    ;
+  \end{rail}
+
+  \begin{descr}
+  
+  \item [\mbox{\isa{\isacommand{case}}}~\isa{{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}}]
+  invokes a named local context \isa{c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m}, as provided by an appropriate
+  proof method (such as \indexref{}{method}{cases}\mbox{\isa{cases}} and \indexref{}{method}{induct}\mbox{\isa{induct}}).
+  The command ``\mbox{\isa{\isacommand{case}}}~\isa{{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}~\mbox{\isa{\isacommand{assume}}}~\isa{c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}''.
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}] prints all local contexts of the
+  current state, using Isar proof language notation.
+  
+  \item [\mbox{\isa{case{\isacharunderscore}names}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k}]
+  declares names for the local contexts of premises of a theorem;
+  \isa{c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k} refers to the \emph{suffix} of the
+  list of premises.
+  
+  \item [\mbox{\isa{case{\isacharunderscore}conclusion}}~\isa{c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k}] declares names for the conclusions of a named premise
+  \isa{c}; here \isa{d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k} refers to the
+  prefix of arguments of a logical formula built by nesting a binary
+  connective (e.g.\ \isa{{\isasymor}}).
+  
+  Note that proof methods such as \mbox{\isa{induct}} and \mbox{\isa{coinduct}} already provide a default name for the conclusion as a
+  whole.  The need to name subformulas only arises with cases that
+  split into several sub-cases, as in common co-induction rules.
+
+  \item [\mbox{\isa{params}}~\isa{p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n}] renames the innermost parameters of
+  premises \isa{{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n} of some theorem.  An empty list of names
+  may be given to skip positions, leaving the present parameters
+  unchanged.
+  
+  Note that the default usage of case rules does \emph{not} directly
+  expose parameters to the proof context.
+  
+  \item [\mbox{\isa{consumes}}~\isa{n}] declares the number of
+  ``major premises'' of a rule, i.e.\ the number of facts to be
+  consumed when it is applied by an appropriate proof method.  The
+  default value of \mbox{\isa{consumes}} is \isa{n\ {\isacharequal}\ {\isadigit{1}}}, which is
+  appropriate for the usual kind of cases and induction rules for
+  inductive sets (cf.\ \secref{sec:hol-inductive}).  Rules without any
+  \mbox{\isa{consumes}} declaration given are treated as if
+  \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} had been specified.
+  
+  Note that explicit \mbox{\isa{consumes}} declarations are only
+  rarely needed; this is already taken care of automatically by the
+  higher-level \mbox{\isa{cases}}, \mbox{\isa{induct}}, and
+  \mbox{\isa{coinduct}} declarations.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Proof methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{method}{cases}\mbox{\isa{cases}} & : & \isarmeth \\
+    \indexdef{}{method}{induct}\mbox{\isa{induct}} & : & \isarmeth \\
+    \indexdef{}{method}{coinduct}\mbox{\isa{coinduct}} & : & \isarmeth \\
+  \end{matharray}
+
+  The \mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}
+  methods provide a uniform interface to common proof techniques over
+  datatypes, inductive predicates (or sets), recursive functions etc.
+  The corresponding rules may be specified and instantiated in a
+  casual manner.  Furthermore, these methods provide named local
+  contexts that may be invoked via the \mbox{\isa{\isacommand{case}}} proof command
+  within the subsequent proof text.  This accommodates compact proof
+  texts even when reasoning about large specifications.
+
+  The \mbox{\isa{induct}} method also provides some additional
+  infrastructure in order to be applicable to structure statements
+  (either using explicit meta-level connectives, or including facts
+  and parameters separately).  This avoids cumbersome encoding of
+  ``strengthened'' inductive statements within the object-logic.
+
+  \begin{rail}
+    'cases' (insts * 'and') rule?
+    ;
+    'induct' (definsts * 'and') \\ arbitrary? taking? rule?
+    ;
+    'coinduct' insts taking rule?
+    ;
+
+    rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
+    ;
+    definst: name ('==' | equiv) term | inst
+    ;
+    definsts: ( definst *)
+    ;
+    arbitrary: 'arbitrary' ':' ((term *) 'and' +)
+    ;
+    taking: 'taking' ':' insts
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{cases}}~\isa{insts\ R}] applies method \mbox{\isa{rule}} with an appropriate case distinction theorem, instantiated to
+  the subjects \isa{insts}.  Symbolic case names are bound according
+  to the rule's local contexts.
+
+  The rule is determined as follows, according to the facts and
+  arguments passed to the \mbox{\isa{cases}} method:
+
+  \medskip
+  \begin{tabular}{llll}
+    facts    &                 & arguments & rule \\\hline
+             & \mbox{\isa{cases}} &           & classical case split \\
+             & \mbox{\isa{cases}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\
+    \isa{{\isasymturnstile}\ A\ t} & \mbox{\isa{cases}} & \isa{{\isasymdots}} & inductive predicate/set elimination (of \isa{A}) \\
+    \isa{{\isasymdots}} & \mbox{\isa{cases}} & \isa{{\isasymdots}\ rule{\isacharcolon}\ R} & explicit rule \isa{R} \\
+  \end{tabular}
+  \medskip
+
+  Several instantiations may be given, referring to the \emph{suffix}
+  of premises of the case rule; within each premise, the \emph{prefix}
+  of variables is instantiated.  In most situations, only a single
+  term needs to be specified; this refers to the first variable of the
+  last premise (it is usually the same for all cases).
+
+  \item [\mbox{\isa{induct}}~\isa{insts\ R}] is analogous to the
+  \mbox{\isa{cases}} method, but refers to induction rules, which are
+  determined as follows:
+
+  \medskip
+  \begin{tabular}{llll}
+    facts    &        & arguments & rule \\\hline
+             & \mbox{\isa{induct}} & \isa{P\ x\ {\isasymdots}} & datatype induction (type of \isa{x}) \\
+    \isa{{\isasymturnstile}\ A\ x} & \mbox{\isa{induct}} & \isa{{\isasymdots}} & predicate/set induction (of \isa{A}) \\
+    \isa{{\isasymdots}} & \mbox{\isa{induct}} & \isa{{\isasymdots}\ rule{\isacharcolon}\ R} & explicit rule \isa{R} \\
+  \end{tabular}
+  \medskip
+  
+  Several instantiations may be given, each referring to some part of
+  a mutual inductive definition or datatype --- only related partial
+  induction rules may be used together, though.  Any of the lists of
+  terms \isa{P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}} refers to the \emph{suffix} of variables
+  present in the induction rule.  This enables the writer to specify
+  only induction variables, or both predicates and variables, for
+  example.
+  
+  Instantiations may be definitional: equations \isa{x\ {\isasymequiv}\ t}
+  introduce local definitions, which are inserted into the claim and
+  discharged after applying the induction rule.  Equalities reappear
+  in the inductive cases, but have been transformed according to the
+  induction principle being involved here.  In order to achieve
+  practically useful induction hypotheses, some variables occurring in
+  \isa{t} need to be fixed (see below).
+  
+  The optional ``\isa{arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}''
+  specification generalizes variables \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m} of the original goal before applying induction.  Thus
+  induction hypotheses may become sufficiently general to get the
+  proof through.  Together with definitional instantiations, one may
+  effectively perform induction over expressions of a certain
+  structure.
+  
+  The optional ``\isa{taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}''
+  specification provides additional instantiations of a prefix of
+  pending variables in the rule.  Such schematic induction rules
+  rarely occur in practice, though.
+
+  \item [\mbox{\isa{coinduct}}~\isa{inst\ R}] is analogous to the
+  \mbox{\isa{induct}} method, but refers to coinduction rules, which are
+  determined as follows:
+
+  \medskip
+  \begin{tabular}{llll}
+    goal     &          & arguments & rule \\\hline
+             & \mbox{\isa{coinduct}} & \isa{x\ {\isasymdots}} & type coinduction (type of \isa{x}) \\
+    \isa{A\ x} & \mbox{\isa{coinduct}} & \isa{{\isasymdots}} & predicate/set coinduction (of \isa{A}) \\
+    \isa{{\isasymdots}} & \mbox{\isa{coinduct}} & \isa{{\isasymdots}\ R} & explicit rule \isa{R} \\
+  \end{tabular}
+  
+  Coinduction is the dual of induction.  Induction essentially
+  eliminates \isa{A\ x} towards a generic result \isa{P\ x},
+  while coinduction introduces \isa{A\ x} starting with \isa{B\ x}, for a suitable ``bisimulation'' \isa{B}.  The cases of a
+  coinduct rule are typically named after the predicates or sets being
+  covered, while the conclusions consist of several alternatives being
+  named after the individual destructor patterns.
+  
+  The given instantiation refers to the \emph{suffix} of variables
+  occurring in the rule's major premise, or conclusion if unavailable.
+  An additional ``\isa{taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}''
+  specification may be required in order to specify the bisimulation
+  to be used in the coinduction step.
+
+  \end{descr}
+
+  Above methods produce named local contexts, as determined by the
+  instantiated rule as given in the text.  Beyond that, the \mbox{\isa{induct}} and \mbox{\isa{coinduct}} methods guess further instantiations
+  from the goal specification itself.  Any persisting unresolved
+  schematic variables of the resulting rule will render the the
+  corresponding case invalid.  The term binding \mbox{\isa{{\isacharquery}case}} for
+  the conclusion will be provided with each case, provided that term
+  is fully specified.
+
+  The \mbox{\isa{\isacommand{print{\isacharunderscore}cases}}} command prints all named cases present
+  in the current proof state.
+
+  \medskip Despite the additional infrastructure, both \mbox{\isa{cases}}
+  and \mbox{\isa{coinduct}} merely apply a certain rule, after
+  instantiation, while conforming due to the usual way of monotonic
+  natural deduction: the context of a structured statement \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}}
+  reappears unchanged after the case split.
+
+  The \mbox{\isa{induct}} method is fundamentally different in this
+  respect: the meta-level structure is passed through the
+  ``recursive'' course involved in the induction.  Thus the original
+  statement is basically replaced by separate copies, corresponding to
+  the induction hypotheses and conclusion; the original goal context
+  is no longer available.  Thus local assumptions, fixed parameters
+  and definitions effectively participate in the inductive rephrasing
+  of the original statement.
+
+  In induction proofs, local assumptions introduced by cases are split
+  into two different kinds: \isa{hyps} stemming from the rule and
+  \isa{prems} from the goal statement.  This is reflected in the
+  extracted cases accordingly, so invoking ``\mbox{\isa{\isacommand{case}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
+  as well as fact \isa{c} to hold the all-inclusive list.
+
+  \medskip Facts presented to either method are consumed according to
+  the number of ``major premises'' of the rule involved, which is
+  usually 0 for plain cases and induction rules of datatypes etc.\ and
+  1 for rules of inductive predicates or sets and the like.  The
+  remaining facts are inserted into the goal verbatim before the
+  actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
+  applied.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Declaring rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{command}{print-induct-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{}{attribute}{cases}\mbox{\isa{cases}} & : & \isaratt \\
+    \indexdef{}{attribute}{induct}\mbox{\isa{induct}} & : & \isaratt \\
+    \indexdef{}{attribute}{coinduct}\mbox{\isa{coinduct}} & : & \isaratt \\
+  \end{matharray}
+
+  \begin{rail}
+    'cases' spec
+    ;
+    'induct' spec
+    ;
+    'coinduct' spec
+    ;
+
+    spec: ('type' | 'pred' | 'set') ':' nameref
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}] prints cases and induct
+  rules for predicates (or sets) and types of the current context.
+  
+  \item [\mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}] (as attributes) augment the corresponding context of
+  rules for reasoning about (co)inductive predicates (or sets) and
+  types, using the corresponding methods of the same name.  Certain
+  definitional packages of object-logics usually declare emerging
+  cases and induction rules as expected, so users rarely need to
+  intervene.
+  
+  Manual rule declarations usually refer to the \mbox{\isa{case{\isacharunderscore}names}} and \mbox{\isa{params}} attributes to adjust names of
+  cases and parameters of a rule; the \mbox{\isa{consumes}}
+  declaration is taken care of automatically: \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \mbox{\isa{consumes}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
+
+  \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:




