--- /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: