diff -r 22dcf2fc0aa2 -r 8fcf19f2168b doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Mon Jun 02 22:50:27 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon Jun 02 22:50:29 2008 +0200 @@ -24,733 +24,7 @@ } \isamarkuptrue% % -\isamarkupsection{Specification commands% -} -\isamarkuptrue% -% -\isamarkupsubsection{Derived specifications% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcll} - \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ - \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\ - \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\ - \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\ - \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\ - \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{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 \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\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 [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] 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 [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an - internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} 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 \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the - object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not - change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup. - - Definitions may be presented with explicit arguments on the LHS, as - well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of - \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an - unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}. - - \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] 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 - ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax - declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in - \secref{sec:syn-trans}. - - \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations - of the current context. - - \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix - syntax with an existing constant or fixed variable. This is a - robust interface to the underlying \hyperlink{command.syntax}{\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 [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\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}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\ - \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{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 [\hyperlink{command.declaration}{\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 [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the - current local theory context. No theorem binding is involved here, - unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\ - \secref{sec:axms-thms}), so \hyperlink{command.declare}{\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{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the - global theory context. - - \begin{matharray}{rcll} - \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ - \indexdef{}{command}{end}\hypertarget{command.end}{\hyperlink{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 [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an - existing locale or class context \isa{c}. Note that locale and - class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} - keyword as well, in order to continue the local theory immediately - after the initial specification. - - \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory and - continues the enclosing global theory. Note that a non-local - \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory - itself (\secref{sec:begin-thy}). - - \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command - specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or - global theory context; the current target context will be suspended - for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' 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{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}. - - 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{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory - level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local - abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} 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{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary - \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.% -\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}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ - \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\ - \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{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 [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] 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 \hyperlink{command.locale}{\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{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed - parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; 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{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (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 [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local - parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both - are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced - implicitly in this context. - - \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type - constraint \isa{{\isasymtau}} on the local parameter \isa{x}. - - \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] - introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a - proof (cf.\ \secref{sec:proof-context}). - - \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously - declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a - proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} - takes an equational proposition instead of variable-term pair. The - left-hand side of the equation may have additional arguments, e.g.\ - ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''. - - \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] - reconsiders facts within a local context. Most notably, this may - include arbitrary declarations in any attribute specifications - included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule. - - \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{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{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given - in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{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{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} 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{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} 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 [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the - specified locale expression in a flattened form. The notable - special case \hyperlink{command.print-locale}{\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 \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default. - Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included. - - \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales - of the current theory. - - \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}] - repeatedly expand all introduction rules of locale predicates of the - theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to - assumptions, \hyperlink{method.unfold-locales}{\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 - \hyperlink{element.includes}{\mbox{\isa{\isakeyword{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 \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}). - - \begin{matharray}{rcl} - \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\ - \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ - \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \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 [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}] - - The first form of \hyperlink{command.interpretation}{\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. - - 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 \hyperlink{keyword.where}{\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 [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}] - - 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 [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}] - interprets \isa{expr} in the proof context and is otherwise - similar to interpretation in theories. - - \item [\hyperlink{command.print-interps}{\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}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ - \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ - \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ - \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ - \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{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 [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines - a new class \isa{c}, inheriting from \isa{superclasses}. This - introduces a locale \isa{c} with import of all locales \isa{superclasses}. - - Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global - theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter - \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}. - - Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted, - mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its - corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The - corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly - --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of - class membership proofs. - - \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\ - \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the - particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\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}\hyperlink{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 [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets - up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro-classes}{\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 [\hyperlink{command.subclass}{\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 [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current - theory. - - \item [\hyperlink{method.intro-classes}{\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 \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular, - instantiation of trivial (syntactic) classes may be performed by a - single ``\hyperlink{command.ddot}{\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{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the - local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} - are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} - referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. - - \item Local theorem bindings are lifted as are assumptions. - - \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and - global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} 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}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\ - \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{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 [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] 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 \hyperlink{method.intro-classes}{\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{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix; - the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}. - - \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and - \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] - setup a goal stating a class relation or type arity. The proof - would usually proceed by \hyperlink{method.intro-classes}{\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 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see - \secref{sec:class}). Sometimes low-level overloading is desirable. - The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for - end-users. - - \begin{matharray}{rcl} - \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{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 [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}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\ {\isasymBEGIN}{\isachardoublequote}}] - 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{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type - instances. The definitions themselves are established using common - specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as - reference to the corresponding constants. The target is concluded - by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}. - - A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} 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% +\isamarkupsection{Configuration options% } \isamarkuptrue% % @@ -790,7 +64,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Proof tools% +\isamarkupsection{Basic proof tools% } \isamarkuptrue% % @@ -1031,11 +305,11 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{The Simplifier \label{sec:simplifier}% +\isamarkupsection{The Simplifier \label{sec:simplifier}% } \isamarkuptrue% % -\isamarkupsubsubsection{Simplification methods% +\isamarkupsubsection{Simplification methods% } \isamarkuptrue% % @@ -1110,7 +384,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Declaring rules% +\isamarkupsubsection{Declaring rules% } \isamarkuptrue% % @@ -1143,7 +417,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Simplification procedures% +\isamarkupsubsection{Simplification procedures% } \isamarkuptrue% % @@ -1189,7 +463,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Forward simplification% +\isamarkupsubsection{Forward simplification% } \isamarkuptrue% % @@ -1224,7 +498,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Low-level equational reasoning% +\isamarkupsubsection{Low-level equational reasoning% } \isamarkuptrue% % @@ -1290,11 +564,11 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{The Classical Reasoner \label{sec:classical}% +\isamarkupsection{The Classical Reasoner \label{sec:classical}% } \isamarkuptrue% % -\isamarkupsubsubsection{Basic methods% +\isamarkupsubsection{Basic methods% } \isamarkuptrue% % @@ -1339,7 +613,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Automated methods% +\isamarkupsubsection{Automated methods% } \isamarkuptrue% % @@ -1384,7 +658,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Combined automated methods \label{sec:clasimp}% +\isamarkupsubsection{Combined automated methods \label{sec:clasimp}% } \isamarkuptrue% % @@ -1430,7 +704,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Declaring rules% +\isamarkupsubsection{Declaring rules% } \isamarkuptrue% % @@ -1486,7 +760,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Classical operations% +\isamarkupsubsection{Classical operations% } \isamarkuptrue% % @@ -1504,355 +778,6 @@ \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}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isartrans{proof(state)}{proof(state)} \\ - \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ - \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\ - \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\ - \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isaratt \\ - \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isaratt \\ - \end{matharray} - - The puristic way to build up Isar proof contexts is by explicit - language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, - \hyperlink{command.let}{\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 \hyperlink{command.case}{\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{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. Term bindings may be covered as well, notably - \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion. - - By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} 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 ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' 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 \hyperlink{command.case}{\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{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}} - for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} 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 - \hyperlink{command.inductive}{\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 [\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}] - invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate - proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}). - The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. - - \item [\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the - current state, using Isar proof language notation. - - \item [\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}] - declares names for the local contexts of premises of a theorem; - \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the - list of premises. - - \item [\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise - \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the - prefix of arguments of a logical formula built by nesting a binary - connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}). - - Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\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 [\hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of - premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} 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 [\hyperlink{attribute.consumes}{\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 \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is - appropriate for the usual kind of cases and induction rules for - inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any - \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if - \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified. - - Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only - rarely needed; this is already taken care of automatically by the - higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and - \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations. - - \end{descr}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Proof methods% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcl} - \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isarmeth \\ - \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isarmeth \\ - \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isarmeth \\ - \end{matharray} - - The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\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 \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command - within the subsequent proof text. This accommodates compact proof - texts even when reasoning about large specifications. - - The \hyperlink{method.induct}{\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 [\hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \hyperlink{method.rule}{\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 \hyperlink{method.cases}{\mbox{\isa{cases}}} method: - - \medskip - \begin{tabular}{llll} - facts & & arguments & rule \\\hline - & \hyperlink{method.cases}{\mbox{\isa{cases}}} & & classical case split \\ - & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\ - \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\ - \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & 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 [\hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the - \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are - determined as follows: - - \medskip - \begin{tabular}{llll} - facts & & arguments & rule \\\hline - & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\ - \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\ - \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & 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{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} 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{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} - 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{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}'' - specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} 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{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}'' - specification provides additional instantiations of a prefix of - pending variables in the rule. Such schematic induction rules - rarely occur in practice, though. - - \item [\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the - \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are - determined as follows: - - \medskip - \begin{tabular}{llll} - goal & & arguments & rule \\\hline - & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\ - \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\ - \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\ - \end{tabular} - - Coinduction is the dual of induction. Induction essentially - eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}}, - while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, 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{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}'' - 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 \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\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 \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for - the conclusion will be provided with each case, provided that term - is fully specified. - - The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present - in the current proof state. - - \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}} - and \hyperlink{method.coinduct}{\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{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}} - reappears unchanged after the case split. - - The \hyperlink{method.induct}{\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 ``\hyperlink{command.case}{\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}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isaratt \\ - \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isaratt \\ - \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{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 [\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct - rules for predicates (or sets) and types of the current context. - - \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\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 \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of - cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} - declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules. - - \end{descr}% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{General logic setup \label{sec:object-logic}% } \isamarkuptrue%