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