# HG changeset patch # User wenzelm # Date 1212439823 -7200 # Node ID 3d3e6e07b93128490ad150c425e01db478f14548 # Parent 14582233d36bfd86b96937dffdea274ab00d67aa major reorganization of document structure; diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/Generic.thy Mon Jun 02 22:50:23 2008 +0200 @@ -6,746 +6,7 @@ chapter {* Generic tools and packages \label{ch:gen-tools} *} -section {* Specification commands *} - -subsection {* Derived specifications *} - -text {* - \begin{matharray}{rcll} - @{command_def "axiomatization"} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ - @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\ - @{attribute_def "defn"} & : & \isaratt \\ - @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "no_notation"} & : & \isarkeep{local{\dsh}theory} \\ - \end{matharray} - - These specification mechanisms provide a slightly more abstract view - than the underlying primitives of @{command "consts"}, @{command - "defs"} (see \secref{sec:consts}), and @{command "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 [@{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m - \ \\<^sub>1 \ \\<^sub>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 [@{command "definition"}~@{text "c \ eq"}] produces an - internal definition @{text "c \ t"} according to the specification - given as @{text 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 @{attribute defn} by the - object-logic. This usually covers object-level equality @{text "x = - y"} and equivalence @{text "A \ B"}. End-users normally need not - change the @{attribute defn} setup. - - Definitions may be presented with explicit arguments on the LHS, as - well as additional conditions, e.g.\ @{text "f x y = t"} instead of - @{text "f \ \x y. t"} and @{text "y \ 0 \ g x y = u"} instead of an - unrestricted @{text "g \ \x y. u"}. - - \item [@{command "abbreviation"}~@{text "c \ eq"}] introduces - a syntactic constant which is associated with a certain term - according to the meta-level equality @{text 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 @{text mode} specification restricts output to a - particular print mode; using ``@{text input}'' here achieves the - effect of one-way abbreviations. The mode may also include an - ``@{keyword "output"}'' qualifier that affects the concrete syntax - declared for abbreviations, cf.\ @{command "syntax"} in - \secref{sec:syn-trans}. - - \item [@{command "print_abbrevs"}] prints all constant abbreviations - of the current context. - - \item [@{command "notation"}~@{text "c (mx)"}] associates mixfix - syntax with an existing constant or fixed variable. This is a - robust interface to the underlying @{command "syntax"} primitive - (\secref{sec:syn-trans}). Type declaration and internal syntactic - representation of the given entity is retrieved from the context. - - \item [@{command "no_notation"}] is similar to @{command - "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}). -*} - - -subsection {* Generic declarations *} - -text {* - 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} - @{command_def "declaration"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "declare"} & : & \isarkeep{local{\dsh}theory} \\ - \end{matharray} - - \begin{rail} - 'declaration' target? text - ; - 'declare' target? (thmrefs + 'and') - ; - \end{rail} - - \begin{descr} - - \item [@{command "declaration"}~@{text d}] adds the declaration - function @{text d} of ML type @{ML_type 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 [@{command "declare"}~@{text thms}] declares theorems to the - current local theory context. No theorem binding is involved here, - unlike @{command "theorems"} or @{command "lemmas"} (cf.\ - \secref{sec:axms-thms}), so @{command "declare"} only has the effect - of applying attributes as included in the theorem specification. - - \end{descr} -*} - - -subsection {* Local theory targets \label{sec:target} *} - -text {* - 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 ``@{text "-"}'' signifies the - global theory context. - - \begin{matharray}{rcll} - @{command_def "context"} & : & \isartrans{theory}{local{\dsh}theory} \\ - @{command_def "end"} & : & \isartrans{local{\dsh}theory}{theory} \\ - \end{matharray} - - \indexouternonterm{target} - \begin{rail} - 'context' name 'begin' - ; - - target: '(' 'in' name ')' - ; - \end{rail} - - \begin{descr} - - \item [@{command "context"}~@{text "c \"}] recommences an - existing locale or class context @{text c}. Note that locale and - class definitions allow to include the @{keyword_ref "begin"} - keyword as well, in order to continue the local theory immediately - after the initial specification. - - \item [@{command "end"}] concludes the current local theory and - continues the enclosing global theory. Note that a non-local - @{command "end"} has a different meaning: it concludes the theory - itself (\secref{sec:begin-thy}). - - \item [@{text "(\ c)"}] given after any local theory command - specifies an immediate target, e.g.\ ``@{command - "definition"}~@{text "(\ c) \"}'' or ``@{command - "theorem"}~@{text "(\ c) \"}''. This works both in a local or - global theory context; the current target context will be suspended - for this command only. Note that ``@{text "(\ -)"}'' 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 - @{text c} with parameter @{text x} and assumption @{text "A[x]"}. - - 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, - @{text "a \ t[x]"} becomes @{text "c.a ?x \ t[?x]"} at the theory - level (for arbitrary @{text "?x"}), together with a local - abbreviation @{text "c \ c.a x"} in the target context (for the - fixed parameter @{text x}). - - Theorems are exported by discharging the assumptions and - generalizing the parameters of the context. For example, @{text "a: - B[x]"} becomes @{text "c.a: A[?x] \ B[?x]"}, again for arbitrary - @{text "?x"}. -*} - - -subsection {* Locales \label{sec:locale} *} - -text {* - 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}). -*} - - -subsubsection {* Locale specifications *} - -text {* - \begin{matharray}{rcl} - @{command_def "locale"} & : & \isartrans{theory}{local{\dsh}theory} \\ - @{command_def "print_locale"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "print_locales"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{method_def intro_locales} & : & \isarmeth \\ - @{method_def unfold_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 [@{command "locale"}~@{text "loc = import + body"}] defines a - new locale @{text loc} as a context consisting of a certain view of - existing locales (@{text import}) plus some additional elements - (@{text body}). Both @{text import} and @{text body} are optional; - the degenerate form @{command "locale"}~@{text 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 @{text import} consists of a structured context expression, - consisting of references to existing locales, renamed contexts, or - merged contexts. Renaming uses positional notation: @{text "c - x\<^sub>1 \ x\<^sub>n"} means that (a prefix of) the fixed - parameters of context @{text c} are named @{text "x\<^sub>1, \, - x\<^sub>n"}; a ``@{text _}'' (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 ``@{text - "(\)"}'' (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 @{text body} consists of basic context elements, further context - expressions may be included as well. - - \begin{descr} - - \item [@{element "fixes"}~@{text "x :: \ (mx)"}] declares a local - parameter of type @{text \} and mixfix annotation @{text mx} (both - are optional). The special syntax declaration ``@{text - "(\)"}'' means that @{text x} may be referenced - implicitly in this context. - - \item [@{element "constrains"}~@{text "x :: \"}] introduces a type - constraint @{text \} on the local parameter @{text x}. - - \item [@{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"}] - introduces local premises, similar to @{command "assume"} within a - proof (cf.\ \secref{sec:proof-context}). - - \item [@{element "defines"}~@{text "a: x \ t"}] defines a previously - declared parameter. This is similar to @{command "def"} within a - proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} - takes an equational proposition instead of variable-term pair. The - left-hand side of the equation may have additional arguments, e.g.\ - ``@{element "defines"}~@{text "f x\<^sub>1 \ x\<^sub>n \ t"}''. - - \item [@{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] - reconsiders facts within a local context. Most notably, this may - include arbitrary declarations in any attribute specifications - included here, e.g.\ a local @{attribute simp} rule. - - \item [@{element "includes"}~@{text 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 @{text 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 ``@{text "(\ p\<^sub>1 \ p\<^sub>n)"}'' patterns given - in the syntax of @{element "assumes"} and @{element "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 @{text - loc_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 @{text 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 @{text \} by @{text \}, and - @{text "\"} by @{text "\"} in HOL; see also - \secref{sec:object-logic}). Separate introduction rules @{text - loc_axioms.intro} and @{text loc.intro} are provided as well. - - The @{text "(open)"} option of a locale specification prevents both - the current @{text loc_axioms} and cumulative @{text loc} predicate - constructions. Predicates are also omitted for empty specification - texts. - - \item [@{command "print_locale"}~@{text "import + body"}] prints the - specified locale expression in a flattened form. The notable - special case @{command "print_locale"}~@{text 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 @{element "notes"} elements by default. - Use @{command "print_locale"}@{text "!"} to get them included. - - \item [@{command "print_locales"}] prints the names of all locales - of the current theory. - - \item [@{method intro_locales} and @{method unfold_locales}] - repeatedly expand all introduction rules of locale predicates of the - theory. While @{method intro_locales} only applies the @{text - loc.intro} introduction rules and therefore does not decend to - assumptions, @{method unfold_locales} is more aggressive and applies - @{text loc_axioms.intro} as well. Both methods are aware of locale - specifications entailed by the context, both from target and - @{element "includes"} statements, and from interpretations (see - below). New goals that are entailed by the current context are - discharged automatically. - - \end{descr} -*} - - -subsubsection {* Interpretation of locales *} - -text {* - 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 @{command - "interpretation"}) and also within a proof body (command @{command - "interpret"}). - - \begin{matharray}{rcl} - @{command_def "interpretation"} & : & \isartrans{theory}{proof(prove)} \\ - @{command_def "interpret"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ - @{command_def "print_interps"}@{text "\<^sup>*"} & : & \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 [@{command "interpretation"}~@{text "expr insts \ eqns"}] - - The first form of @{command "interpretation"} interprets @{text - expr} in the theory. The instantiation is given as a list of terms - @{text 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 ``@{text _}'' 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 @{keyword "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 [@{command "interpretation"}~@{text "name \ expr"}] - - This form of the command interprets @{text expr} in the locale - @{text name}. It requires a proof that the specification of @{text - name} implies the specification of @{text expr}. As in the - localized version of the theorem command, the proof is in the - context of @{text name}. After the proof obligation has been - dischared, the facts of @{text expr} become part of locale @{text - name} as \emph{derived} context elements and are available when the - context @{text name} is subsequently entered. Note that, like - import, this is dynamic: facts added to a locale part of @{text - expr} after interpretation become also available in @{text 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 ``@{text _}''). - - Unlike interpretation in theories, instantiation is confined to the - renaming of parameters, which may be specified as part of the - context expression @{text expr}. Using defined parameters in @{text - name} one may achieve an effect similar to instantiation, though. - - Only specification fragments of @{text expr} that are not already - part of @{text name} (be it imported, derived or a derived fragment - of the import) are considered by interpretation. This enables - circular interpretations. - - If interpretations of @{text name} exist in the current theory, the - command adds interpretations for @{text expr} as well, with the same - prefix and attributes, although only for fragments of @{text expr} - that are not interpreted in the theory already. - - \item [@{command "interpret"}~@{text "expr insts \ eqns"}] - interprets @{text expr} in the proof context and is otherwise - similar to interpretation in theories. - - \item [@{command "print_interps"}~@{text loc}] prints the - interpretations of a particular locale @{text 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} -*} - - -subsection {* Classes \label{sec:class} *} - -text {* - A class is a particular locale with \emph{exactly one} type variable - @{text \}. 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} - @{command_def "class"} & : & \isartrans{theory}{local{\dsh}theory} \\ - @{command_def "instantiation"} & : & \isartrans{theory}{local{\dsh}theory} \\ - @{command_def "instance"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ - @{command_def "subclass"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ - @{command_def "print_classes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{method_def intro_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 [@{command "class"}~@{text "c = superclasses + body"}] defines - a new class @{text c}, inheriting from @{text superclasses}. This - introduces a locale @{text c} with import of all locales @{text - superclasses}. - - Any @{element "fixes"} in @{text body} are lifted to the global - theory level (\emph{class operations} @{text "f\<^sub>1, \, - f\<^sub>n"} of class @{text c}), mapping the local type parameter - @{text \} to a schematic type variable @{text "?\ :: c"}. - - Likewise, @{element "assumes"} in @{text body} are also lifted, - mapping each local parameter @{text "f :: \[\]"} to its - corresponding global constant @{text "f :: \[?\ :: c]"}. The - corresponding introduction rule is provided as @{text - c_class_axioms.intro}. This rule should be rarely needed directly - --- the @{method intro_classes} method takes care of the details of - class membership proofs. - - \item [@{command "instantiation"}~@{text "t :: (s\<^sub>1, \, - s\<^sub>n) s \"}] opens a theory target (cf.\ - \secref{sec:target}) which allows to specify class operations @{text - "f\<^sub>1, \, f\<^sub>n"} corresponding to sort @{text s} at the - particular type instance @{text "(\\<^sub>1 :: s\<^sub>1, \, - \\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command - in the target body poses a goal stating these type arities. The - target is concluded by an @{command_ref "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 [@{command "instance"}] in an instantiation target body sets - up a goal stating the type arities claimed at the opening @{command - "instantiation"}. The proof would usually proceed by @{method - intro_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 [@{command "subclass"}~@{text c}] in a class context for class - @{text d} sets up a goal stating that class @{text c} is logically - contained in class @{text d}. After finishing the proof, class - @{text d} is proven to be subclass @{text c} and the locale @{text - c} is interpreted into @{text d} simultaneously. - - \item [@{command "print_classes"}] prints all classes in the current - theory. - - \item [@{method intro_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 @{command "proof"}). In particular, - instantiation of trivial (syntactic) classes may be performed by a - single ``@{command ".."}'' proof step. - - \end{descr} -*} - - -subsubsection {* The class target *} - -text {* - %FIXME check - - A named context may refer to a locale (cf.\ \secref{sec:target}). - If this locale is also a class @{text c}, apart from the common - locale target behaviour the following happens. - - \begin{itemize} - - \item Local constant declarations @{text "g[\]"} referring to the - local type parameter @{text \} and local parameters @{text "f[\]"} - are accompanied by theory-level constants @{text "g[?\ :: c]"} - referring to theory-level class operations @{text "f[?\ :: c]"}. - - \item Local theorem bindings are lifted as are assumptions. - - \item Local syntax refers to local operations @{text "g[\]"} and - global operations @{text "g[?\ :: c]"} uniformly. Type inference - resolves ambiguities. In rare cases, manual type annotations are - needed. - - \end{itemize} -*} - - -subsection {* Axiomatic type classes \label{sec:axclass} *} - -text {* - \begin{matharray}{rcl} - @{command_def "axclass"} & : & \isartrans{theory}{theory} \\ - @{command_def "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 [@{command "axclass"}~@{text "c \ c\<^sub>1, \, c\<^sub>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 - @{text c_class.intro}); this rule is employed by method @{method - intro_classes} to support instantiation proofs of this class. - - The ``class axioms'' are stored as theorems according to the given - name specifications, adding @{text "c_class"} as name space prefix; - the same facts are also stored collectively as @{text - c_class.axioms}. - - \item [@{command "instance"}~@{text "c\<^sub>1 \ c\<^sub>2"} and - @{command "instance"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) s"}] - setup a goal stating a class relation or type arity. The proof - would usually proceed by @{method intro_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} -*} - - -subsection {* Arbitrary overloading *} - -text {* - 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 @{command "instantiation"} (see - \secref{sec:class}). Sometimes low-level overloading is desirable. - The @{command "overloading"} target provides a convenient view for - end-users. - - \begin{matharray}{rcl} - @{command_def "overloading"} & : & \isartrans{theory}{local{\dsh}theory} \\ - \end{matharray} - - \begin{rail} - 'overloading' \\ - ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' - \end{rail} - - \begin{descr} - - \item [@{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: - \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"}] - 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 @{text - "x\<^sub>i"} to constants @{text "c\<^sub>i"} at particular type - instances. The definitions themselves are established using common - specification tools, using the names @{text "x\<^sub>i"} as - reference to the corresponding constants. The target is concluded - by @{command "end"}. - - A @{text "(unchecked)"} 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} -*} - - -subsection {* Configuration options *} +section {* Configuration options *} text {* Isabelle/Pure maintains a record of named configuration options @@ -786,7 +47,7 @@ *} -section {* Proof tools *} +section {* Basic proof tools *} subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *} @@ -1031,9 +292,9 @@ *} -subsection {* The Simplifier \label{sec:simplifier} *} +section {* The Simplifier \label{sec:simplifier} *} -subsubsection {* Simplification methods *} +subsection {* Simplification methods *} text {* \begin{matharray}{rcl} @@ -1112,7 +373,7 @@ *} -subsubsection {* Declaring rules *} +subsection {* Declaring rules *} text {* \begin{matharray}{rcl} @@ -1143,7 +404,7 @@ *} -subsubsection {* Simplification procedures *} +subsection {* Simplification procedures *} text {* \begin{matharray}{rcl} @@ -1189,7 +450,7 @@ *} -subsubsection {* Forward simplification *} +subsection {* Forward simplification *} text {* \begin{matharray}{rcl} @@ -1224,7 +485,7 @@ *} -subsubsection {* Low-level equational reasoning *} +subsection {* Low-level equational reasoning *} text {* \begin{matharray}{rcl} @@ -1290,9 +551,9 @@ *} -subsection {* The Classical Reasoner \label{sec:classical} *} +section {* The Classical Reasoner \label{sec:classical} *} -subsubsection {* Basic methods *} +subsection {* Basic methods *} text {* \begin{matharray}{rcl} @@ -1335,7 +596,7 @@ *} -subsubsection {* Automated methods *} +subsection {* Automated methods *} text {* \begin{matharray}{rcl} @@ -1381,7 +642,7 @@ *} -subsubsection {* Combined automated methods \label{sec:clasimp} *} +subsection {* Combined automated methods \label{sec:clasimp} *} text {* \begin{matharray}{rcl} @@ -1427,7 +688,7 @@ *} -subsubsection {* Declaring rules *} +subsection {* Declaring rules *} text {* \begin{matharray}{rcl} @@ -1483,7 +744,7 @@ *} -subsubsection {* Classical operations *} +subsection {* Classical operations *} text {* \begin{matharray}{rcl} @@ -1500,370 +761,6 @@ *} -subsection {* Proof by cases and induction \label{sec:cases-induct} *} - -subsubsection {* Rule contexts *} - -text {* - \begin{matharray}{rcl} - @{command_def "case"} & : & \isartrans{proof(state)}{proof(state)} \\ - @{command_def "print_cases"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ - @{attribute_def case_names} & : & \isaratt \\ - @{attribute_def case_conclusion} & : & \isaratt \\ - @{attribute_def params} & : & \isaratt \\ - @{attribute_def consumes} & : & \isaratt \\ - \end{matharray} - - The puristic way to build up Isar proof contexts is by explicit - language elements like @{command "fix"}, @{command "assume"}, - @{command "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 @{command "case"} command provides a shorthand to refer to a - local context symbolically: certain proof methods provide an - environment of named ``cases'' of the form @{text "c: x\<^sub>1, \, - x\<^sub>m, \\<^sub>1, \, \\<^sub>n"}; the effect of ``@{command - "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text - "x\<^sub>1 \ x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ - \\<^sub>n"}''. Term bindings may be covered as well, notably - @{variable ?case} for the main conclusion. - - By default, the ``terminology'' @{text "x\<^sub>1, \, x\<^sub>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 ``@{command "case"}~@{text "(c - y\<^sub>1 \ y\<^sub>m)"}'' 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 @{command - "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 @{text "goal\<^sub>i"} - for each subgoal @{text "i = 1, \, 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 - @{command "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 [@{command "case"}~@{text "(c x\<^sub>1 \ x\<^sub>m)"}] - invokes a named local context @{text "c: x\<^sub>1, \, x\<^sub>m, - \\<^sub>1, \, \\<^sub>m"}, as provided by an appropriate - proof method (such as @{method_ref cases} and @{method_ref induct}). - The command ``@{command "case"}~@{text "(c x\<^sub>1 \ - x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ - x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ - \\<^sub>n"}''. - - \item [@{command "print_cases"}] prints all local contexts of the - current state, using Isar proof language notation. - - \item [@{attribute case_names}~@{text "c\<^sub>1 \ c\<^sub>k"}] - declares names for the local contexts of premises of a theorem; - @{text "c\<^sub>1, \, c\<^sub>k"} refers to the \emph{suffix} of the - list of premises. - - \item [@{attribute case_conclusion}~@{text "c d\<^sub>1 \ - d\<^sub>k"}] declares names for the conclusions of a named premise - @{text c}; here @{text "d\<^sub>1, \, d\<^sub>k"} refers to the - prefix of arguments of a logical formula built by nesting a binary - connective (e.g.\ @{text "\"}). - - Note that proof methods such as @{method induct} and @{method - 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 [@{attribute params}~@{text "p\<^sub>1 \ p\<^sub>m \ \ - q\<^sub>1 \ q\<^sub>n"}] renames the innermost parameters of - premises @{text "1, \, 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 [@{attribute consumes}~@{text 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 @{attribute consumes} is @{text "n = 1"}, which is - appropriate for the usual kind of cases and induction rules for - inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any - @{attribute consumes} declaration given are treated as if - @{attribute consumes}~@{text 0} had been specified. - - Note that explicit @{attribute consumes} declarations are only - rarely needed; this is already taken care of automatically by the - higher-level @{attribute cases}, @{attribute induct}, and - @{attribute coinduct} declarations. - - \end{descr} -*} - - -subsubsection {* Proof methods *} - -text {* - \begin{matharray}{rcl} - @{method_def cases} & : & \isarmeth \\ - @{method_def induct} & : & \isarmeth \\ - @{method_def coinduct} & : & \isarmeth \\ - \end{matharray} - - The @{method cases}, @{method induct}, and @{method 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 @{command "case"} proof command - within the subsequent proof text. This accommodates compact proof - texts even when reasoning about large specifications. - - The @{method 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 [@{method cases}~@{text "insts R"}] applies method @{method - rule} with an appropriate case distinction theorem, instantiated to - the subjects @{text 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 @{method cases} method: - - \medskip - \begin{tabular}{llll} - facts & & arguments & rule \\\hline - & @{method cases} & & classical case split \\ - & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\ - @{text "\ A t"} & @{method cases} & @{text "\"} & inductive predicate/set elimination (of @{text A}) \\ - @{text "\"} & @{method cases} & @{text "\ rule: R"} & explicit rule @{text 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 [@{method induct}~@{text "insts R"}] is analogous to the - @{method cases} method, but refers to induction rules, which are - determined as follows: - - \medskip - \begin{tabular}{llll} - facts & & arguments & rule \\\hline - & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\ - @{text "\ A x"} & @{method induct} & @{text "\"} & predicate/set induction (of @{text A}) \\ - @{text "\"} & @{method induct} & @{text "\ rule: R"} & explicit rule @{text 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 @{text "P, x, \"} 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 @{text "x \ 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 - @{text t} need to be fixed (see below). - - The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' - specification generalizes variables @{text "x\<^sub>1, \, - x\<^sub>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 ``@{text "taking: t\<^sub>1 \ t\<^sub>n"}'' - specification provides additional instantiations of a prefix of - pending variables in the rule. Such schematic induction rules - rarely occur in practice, though. - - \item [@{method coinduct}~@{text "inst R"}] is analogous to the - @{method induct} method, but refers to coinduction rules, which are - determined as follows: - - \medskip - \begin{tabular}{llll} - goal & & arguments & rule \\\hline - & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\ - @{text "A x"} & @{method coinduct} & @{text "\"} & predicate/set coinduction (of @{text A}) \\ - @{text "\"} & @{method coinduct} & @{text "\ rule: R"} & explicit rule @{text R} \\ - \end{tabular} - - Coinduction is the dual of induction. Induction essentially - eliminates @{text "A x"} towards a generic result @{text "P x"}, - while coinduction introduces @{text "A x"} starting with @{text "B - x"}, for a suitable ``bisimulation'' @{text 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 ``@{text "taking: t\<^sub>1 \ t\<^sub>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 @{method - induct} and @{method 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 @{variable ?case} for - the conclusion will be provided with each case, provided that term - is fully specified. - - The @{command "print_cases"} command prints all named cases present - in the current proof state. - - \medskip Despite the additional infrastructure, both @{method cases} - and @{method 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 @{text - "\x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ \\<^sub>n \ \"} - reappears unchanged after the case split. - - The @{method 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: @{text hyps} stemming from the rule and - @{text prems} from the goal statement. This is reflected in the - extracted cases accordingly, so invoking ``@{command "case"}~@{text - c}'' will provide separate facts @{text c.hyps} and @{text c.prems}, - as well as fact @{text 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 @{text cases}, @{text induct}, or @{text coinduct} rule is - applied. -*} - - -subsubsection {* Declaring rules *} - -text {* - \begin{matharray}{rcl} - @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{attribute_def cases} & : & \isaratt \\ - @{attribute_def induct} & : & \isaratt \\ - @{attribute_def coinduct} & : & \isaratt \\ - \end{matharray} - - \begin{rail} - 'cases' spec - ; - 'induct' spec - ; - 'coinduct' spec - ; - - spec: ('type' | 'pred' | 'set') ':' nameref - ; - \end{rail} - - \begin{descr} - - \item [@{command "print_induct_rules"}] prints cases and induct - rules for predicates (or sets) and types of the current context. - - \item [@{attribute cases}, @{attribute induct}, and @{attribute - 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 @{attribute - case_names} and @{attribute params} attributes to adjust names of - cases and parameters of a rule; the @{attribute consumes} - declaration is taken care of automatically: @{attribute - consumes}~@{text 0} is specified for ``type'' rules and @{attribute - consumes}~@{text 1} for ``predicate'' / ``set'' rules. - - \end{descr} -*} - - section {* General logic setup \label{sec:object-logic} *} text {* diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/Introduction.thy --- a/doc-src/IsarRef/Thy/Introduction.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/Introduction.thy Mon Jun 02 22:50:23 2008 +0200 @@ -53,10 +53,23 @@ \medskip The Isabelle/Isar framework is generic and should work reasonably well for any Isabelle object-logic that conforms to the - natural deduction view of the Isabelle/Pure framework. Major - Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF - \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF - \cite{isabelle-ZF} have already been set up for end-users. + natural deduction view of the Isabelle/Pure framework. Specific + language elements introduced by the major object-logics are + described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf} + (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). The main + language elements are already provided by the Isabelle/Pure + framework. Nevertheless, examples given in the generic parts will + usually refer to Isabelle/HOL as well. + + \medskip Isar commands may be either \emph{proper} document + constructors, or \emph{improper commands}. Some proof methods and + attributes introduced later are classified as improper as well. + Improper Isar language elements, which are marked by ``@{text + "\<^sup>*"}'' in the subsequent chapters; they are often helpful + when developing proof documents, but their use is discouraged for + the final human-readable outcome. Typical examples are diagnostic + commands that print terms or theorems according to the current + context; other commands emulate old-style tactical theorem proving. *} @@ -84,7 +97,7 @@ *} -subsection {* Proof General *} +subsection {* Emacs Proof General *} text {* Plain TTY-based interaction as above used to be quite feasible with @@ -171,7 +184,7 @@ hand, the plain ASCII sources easily become somewhat unintelligible. For example, @{text "\"} would appear as @{verbatim "\"} according the default set of Isabelle symbols. Nevertheless, the Isabelle - document preparation system (see \secref{sec:document-prep}) will be + document preparation system (see \chref{ch:document-prep}) will be happy to print non-ASCII symbols properly. It is even possible to invent additional notation beyond the display capabilities of Emacs and X-Symbol. @@ -214,56 +227,6 @@ *} -subsection {* Document preparation \label{sec:document-prep} *} - -text {* - Isabelle/Isar provides a simple document preparation system based on - existing {PDF-\LaTeX} technology, with full support of hyper-links - (both local references and URLs) and bookmarks. Thus the results - are equally well suited for WWW browsing and as printed copies. - - \medskip Isabelle generates {\LaTeX} output as part of the run of a - \emph{logic session} (see also \cite{isabelle-sys}). Getting - started with a working configuration for common situations is quite - easy by using the Isabelle @{verbatim mkdir} and @{verbatim make} - tools. First invoke -\begin{ttbox} - isatool mkdir Foo -\end{ttbox} - to initialize a separate directory for session @{verbatim Foo} --- - it is safe to experiment, since @{verbatim "isatool mkdir"} never - overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"} - holds ML commands to load all theories required for this session; - furthermore @{verbatim "Foo/document/root.tex"} should include any - special {\LaTeX} macro packages required for your document (the - default is usually sufficient as a start). - - The session is controlled by a separate @{verbatim IsaMakefile} - (with crude source dependencies by default). This file is located - one level up from the @{verbatim Foo} directory location. Now - invoke -\begin{ttbox} - isatool make Foo -\end{ttbox} - to run the @{verbatim Foo} session, with browser information and - document preparation enabled. Unless any errors are reported by - Isabelle or {\LaTeX}, the output will appear inside the directory - @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in - verbose mode. - - \medskip You may also consider to tune the @{verbatim usedir} - options in @{verbatim IsaMakefile}, for example to change the output - format from @{verbatim pdf} to @{verbatim dvi}, or activate the - @{verbatim "-D"} option to retain a second copy of the generated - {\LaTeX} sources. - - \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys} - for further details on Isabelle logic sessions and theory - presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book} - also covers theory presentation issues. -*} - - subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *} text {* diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Jun 02 22:50:23 2008 +0200 @@ -4,7 +4,7 @@ imports Pure begin -chapter {* Syntax primitives *} +chapter {* Outer syntax *} text {* The rather generic framework of Isabelle/Isar syntax emerges from @@ -468,283 +468,4 @@ \secref{sec:proof-context}. *} - -subsection {* Antiquotations \label{sec:antiq} *} - -text {* - \begin{matharray}{rcl} - @{antiquotation_def "theory"} & : & \isarantiq \\ - @{antiquotation_def "thm"} & : & \isarantiq \\ - @{antiquotation_def "prop"} & : & \isarantiq \\ - @{antiquotation_def "term"} & : & \isarantiq \\ - @{antiquotation_def const} & : & \isarantiq \\ - @{antiquotation_def abbrev} & : & \isarantiq \\ - @{antiquotation_def typeof} & : & \isarantiq \\ - @{antiquotation_def typ} & : & \isarantiq \\ - @{antiquotation_def thm_style} & : & \isarantiq \\ - @{antiquotation_def term_style} & : & \isarantiq \\ - @{antiquotation_def "text"} & : & \isarantiq \\ - @{antiquotation_def goals} & : & \isarantiq \\ - @{antiquotation_def subgoals} & : & \isarantiq \\ - @{antiquotation_def prf} & : & \isarantiq \\ - @{antiquotation_def full_prf} & : & \isarantiq \\ - @{antiquotation_def ML} & : & \isarantiq \\ - @{antiquotation_def ML_type} & : & \isarantiq \\ - @{antiquotation_def ML_struct} & : & \isarantiq \\ - \end{matharray} - - The text body of formal comments (see also \secref{sec:comments}) - may contain antiquotations of logical entities, such as theorems, - terms and types, which are to be presented in the final output - produced by the Isabelle document preparation system (see also - \secref{sec:document-prep}). - - Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}'' - within a text block would cause - \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document. Also note that theorem - antiquotations may involve attributes as well. For example, - @{text "@{thm sym [no_vars]}"} would print the theorem's - statement where all schematic variables have been replaced by fixed - ones, which are easier to read. - - \begin{rail} - atsign lbrace antiquotation rbrace - ; - - antiquotation: - 'theory' options name | - 'thm' options thmrefs | - 'prop' options prop | - 'term' options term | - 'const' options term | - 'abbrev' options term | - 'typeof' options term | - 'typ' options type | - 'thm\_style' options name thmref | - 'term\_style' options name term | - 'text' options name | - 'goals' options | - 'subgoals' options | - 'prf' options thmrefs | - 'full\_prf' options thmrefs | - 'ML' options name | - 'ML\_type' options name | - 'ML\_struct' options name - ; - options: '[' (option * ',') ']' - ; - option: name | name '=' name - ; - \end{rail} - - Note that the syntax of antiquotations may \emph{not} include source - comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} or verbatim - text @{verbatim "{"}@{verbatim "*"}~@{text "\"}~@{verbatim - "*"}@{verbatim "}"}. - - \begin{descr} - - \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is - guaranteed to refer to a valid ancestor theory in the current - context. - - \item [@{text "@{thm a\<^sub>1 \ a\<^sub>n}"}] prints theorems - @{text "a\<^sub>1 \ a\<^sub>n"}. Note that attribute specifications - may be included as well (see also \secref{sec:syn-att}); the - @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would - be particularly useful to suppress printing of schematic variables. - - \item [@{text "@{prop \}"}] prints a well-typed proposition @{text - "\"}. - - \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}. - - \item [@{text "@{const c}"}] prints a logical or syntactic constant - @{text "c"}. - - \item [@{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"}] prints a constant - abbreviation @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in - the current context. - - \item [@{text "@{typeof t}"}] prints the type of a well-typed term - @{text "t"}. - - \item [@{text "@{typ \}"}] prints a well-formed type @{text "\"}. - - \item [@{text "@{thm_style s a}"}] prints theorem @{text a}, - previously applying a style @{text s} to it (see below). - - \item [@{text "@{term_style s t}"}] prints a well-typed term @{text - t} after applying a style @{text s} to it (see below). - - \item [@{text "@{text s}"}] prints uninterpreted source text @{text - s}. This is particularly useful to print portions of text according - to the Isabelle {\LaTeX} output style, without demanding - well-formedness (e.g.\ small pieces of terms that should not be - parsed or type-checked yet). - - \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal - state. This is mainly for support of tactic-emulation scripts - within Isar --- presentation of goal states does not conform to - actual human-readable proof documents. - - Please do not include goal states into document output unless you - really know what you are doing! - - \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but - does not print the main goal. - - \item [@{text "@{prf a\<^sub>1 \ a\<^sub>n}"}] prints the (compact) - proof terms corresponding to the theorems @{text "a\<^sub>1 \ - a\<^sub>n"}. Note that this requires proof terms to be switched on - for the current object logic (see the ``Proof terms'' section of the - Isabelle reference manual for information on how to do this). - - \item [@{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"}] is like @{text - "@{prf a\<^sub>1 \ a\<^sub>n}"}, but displays the full proof terms, - i.e.\ also displays information omitted in the compact proof term, - which is denoted by ``@{text _}'' placeholders there. - - \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text - "@{ML_struct s}"}] check text @{text s} as ML value, type, and - structure, respectively. The source is displayed verbatim. - - \end{descr} - - \medskip The following standard styles for use with @{text - thm_style} and @{text term_style} are available: - - \begin{descr} - - \item [@{text lhs}] extracts the first argument of any application - form with at least two arguments -- typically meta-level or - object-level equality, or any other binary relation. - - \item [@{text rhs}] is like @{text lhs}, but extracts the second - argument. - - \item [@{text "concl"}] extracts the conclusion @{text C} from a rule - in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"}. - - \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise - number @{text "1, \, 9"}, respectively, from from a rule in - Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} - - \end{descr} - - \medskip - The following options are available to tune the output. Note that most of - these coincide with ML flags of the same names (see also \cite{isabelle-ref}). - - \begin{descr} - - \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}] - control printing of explicit type and sort constraints. - - \item[@{text "show_structs = bool"}] controls printing of implicit - structures. - - \item[@{text "long_names = bool"}] forces names of types and - constants etc.\ to be printed in their fully qualified internal - form. - - \item[@{text "short_names = bool"}] forces names of types and - constants etc.\ to be printed unqualified. Note that internalizing - the output again in the current context may well yield a different - result. - - \item[@{text "unique_names = bool"}] determines whether the printed - version of qualified names should be made sufficiently long to avoid - overlap with names declared further back. Set to @{text false} for - more concise output. - - \item[@{text "eta_contract = bool"}] prints terms in @{text - \}-contracted form. - - \item[@{text "display = bool"}] indicates if the text is to be - output as multi-line ``display material'', rather than a small piece - of text without line breaks (which is the default). - - \item[@{text "break = bool"}] controls line breaks in non-display - material. - - \item[@{text "quotes = bool"}] indicates if the output should be - enclosed in double quotes. - - \item[@{text "mode = name"}] adds @{text name} to the print mode to - be used for presentation (see also \cite{isabelle-ref}). Note that - the standard setup for {\LaTeX} output is already present by - default, including the modes @{text latex} and @{text xsymbols}. - - \item[@{text "margin = nat"} and @{text "indent = nat"}] change the - margin or indentation for pretty printing of display material. - - \item[@{text "source = bool"}] prints the source text of the - antiquotation arguments, rather than the actual value. Note that - this does not affect well-formedness checks of @{antiquotation - "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation - "text"} antiquotation admits arbitrary output). - - \item[@{text "goals_limit = nat"}] determines the maximum number of - goals to be printed. - - \item[@{text "locale = name"}] specifies an alternative locale - context used for evaluating and printing the subsequent argument. - - \end{descr} - - For boolean flags, ``@{text "name = true"}'' may be abbreviated as - ``@{text name}''. All of the above flags are disabled by default, - unless changed from ML. - - \medskip Note that antiquotations do not only spare the author from - tedious typing of logical entities, but also achieve some degree of - consistency-checking of informal explanations with formal - developments: well-formedness of terms and types with respect to the - current theory or proof context is ensured here. -*} - - -subsection {* Tagged commands \label{sec:tags} *} - -text {* - Each Isabelle/Isar command may be decorated by presentation tags: - - \indexouternonterm{tags} - \begin{rail} - tags: ( tag * ) - ; - tag: '\%' (ident | string) - \end{rail} - - The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already - pre-declared for certain classes of commands: - - \medskip - - \begin{tabular}{ll} - @{text "theory"} & theory begin/end \\ - @{text "proof"} & all proof commands \\ - @{text "ML"} & all commands involving ML code \\ - \end{tabular} - - \medskip The Isabelle document preparation system (see also - \cite{isabelle-sys}) allows tagged command regions to be presented - specifically, e.g.\ to fold proof texts, or drop parts of the text - completely. - - For example ``@{command "by"}~@{text "%invisible auto"}'' would - cause that piece of proof to be treated as @{text invisible} instead - of @{text "proof"} (the default), which may be either show or hidden - depending on the document setup. In contrast, ``@{command - "by"}~@{text "%visible auto"}'' would force this text to be shown - invariably. - - Explicit tag specifications within a proof apply to all subsequent - commands of the same level of nesting. For example, ``@{command - "proof"}~@{text "%visible \"}~@{command "qed"}'' would force the - whole sub-proof to be typeset as @{text visible} (unless some of its - parts are tagged differently). -*} - end diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 02 22:50:23 2008 +0200 @@ -1036,4 +1036,367 @@ \end{descr} *} +section {* Proof by cases and induction \label{sec:cases-induct} *} + +subsection {* Rule contexts *} + +text {* + \begin{matharray}{rcl} + @{command_def "case"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "print_cases"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ + @{attribute_def case_names} & : & \isaratt \\ + @{attribute_def case_conclusion} & : & \isaratt \\ + @{attribute_def params} & : & \isaratt \\ + @{attribute_def consumes} & : & \isaratt \\ + \end{matharray} + + The puristic way to build up Isar proof contexts is by explicit + language elements like @{command "fix"}, @{command "assume"}, + @{command "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 @{command "case"} command provides a shorthand to refer to a + local context symbolically: certain proof methods provide an + environment of named ``cases'' of the form @{text "c: x\<^sub>1, \, + x\<^sub>m, \\<^sub>1, \, \\<^sub>n"}; the effect of ``@{command + "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text + "x\<^sub>1 \ x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ + \\<^sub>n"}''. Term bindings may be covered as well, notably + @{variable ?case} for the main conclusion. + + By default, the ``terminology'' @{text "x\<^sub>1, \, x\<^sub>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 ``@{command "case"}~@{text "(c + y\<^sub>1 \ y\<^sub>m)"}'' 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 @{command + "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 @{text "goal\<^sub>i"} + for each subgoal @{text "i = 1, \, 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 + @{command "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 [@{command "case"}~@{text "(c x\<^sub>1 \ x\<^sub>m)"}] + invokes a named local context @{text "c: x\<^sub>1, \, x\<^sub>m, + \\<^sub>1, \, \\<^sub>m"}, as provided by an appropriate + proof method (such as @{method_ref cases} and @{method_ref induct}). + The command ``@{command "case"}~@{text "(c x\<^sub>1 \ + x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ + x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ + \\<^sub>n"}''. + + \item [@{command "print_cases"}] prints all local contexts of the + current state, using Isar proof language notation. + + \item [@{attribute case_names}~@{text "c\<^sub>1 \ c\<^sub>k"}] + declares names for the local contexts of premises of a theorem; + @{text "c\<^sub>1, \, c\<^sub>k"} refers to the \emph{suffix} of the + list of premises. + + \item [@{attribute case_conclusion}~@{text "c d\<^sub>1 \ + d\<^sub>k"}] declares names for the conclusions of a named premise + @{text c}; here @{text "d\<^sub>1, \, d\<^sub>k"} refers to the + prefix of arguments of a logical formula built by nesting a binary + connective (e.g.\ @{text "\"}). + + Note that proof methods such as @{method induct} and @{method + 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 [@{attribute params}~@{text "p\<^sub>1 \ p\<^sub>m \ \ + q\<^sub>1 \ q\<^sub>n"}] renames the innermost parameters of + premises @{text "1, \, 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 [@{attribute consumes}~@{text 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 @{attribute consumes} is @{text "n = 1"}, which is + appropriate for the usual kind of cases and induction rules for + inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any + @{attribute consumes} declaration given are treated as if + @{attribute consumes}~@{text 0} had been specified. + + Note that explicit @{attribute consumes} declarations are only + rarely needed; this is already taken care of automatically by the + higher-level @{attribute cases}, @{attribute induct}, and + @{attribute coinduct} declarations. + + \end{descr} +*} + + +subsection {* Proof methods *} + +text {* + \begin{matharray}{rcl} + @{method_def cases} & : & \isarmeth \\ + @{method_def induct} & : & \isarmeth \\ + @{method_def coinduct} & : & \isarmeth \\ + \end{matharray} + + The @{method cases}, @{method induct}, and @{method 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 @{command "case"} proof command + within the subsequent proof text. This accommodates compact proof + texts even when reasoning about large specifications. + + The @{method 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 [@{method cases}~@{text "insts R"}] applies method @{method + rule} with an appropriate case distinction theorem, instantiated to + the subjects @{text 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 @{method cases} method: + + \medskip + \begin{tabular}{llll} + facts & & arguments & rule \\\hline + & @{method cases} & & classical case split \\ + & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\ + @{text "\ A t"} & @{method cases} & @{text "\"} & inductive predicate/set elimination (of @{text A}) \\ + @{text "\"} & @{method cases} & @{text "\ rule: R"} & explicit rule @{text 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 [@{method induct}~@{text "insts R"}] is analogous to the + @{method cases} method, but refers to induction rules, which are + determined as follows: + + \medskip + \begin{tabular}{llll} + facts & & arguments & rule \\\hline + & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\ + @{text "\ A x"} & @{method induct} & @{text "\"} & predicate/set induction (of @{text A}) \\ + @{text "\"} & @{method induct} & @{text "\ rule: R"} & explicit rule @{text 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 @{text "P, x, \"} 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 @{text "x \ 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 + @{text t} need to be fixed (see below). + + The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' + specification generalizes variables @{text "x\<^sub>1, \, + x\<^sub>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 ``@{text "taking: t\<^sub>1 \ t\<^sub>n"}'' + specification provides additional instantiations of a prefix of + pending variables in the rule. Such schematic induction rules + rarely occur in practice, though. + + \item [@{method coinduct}~@{text "inst R"}] is analogous to the + @{method induct} method, but refers to coinduction rules, which are + determined as follows: + + \medskip + \begin{tabular}{llll} + goal & & arguments & rule \\\hline + & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\ + @{text "A x"} & @{method coinduct} & @{text "\"} & predicate/set coinduction (of @{text A}) \\ + @{text "\"} & @{method coinduct} & @{text "\ rule: R"} & explicit rule @{text R} \\ + \end{tabular} + + Coinduction is the dual of induction. Induction essentially + eliminates @{text "A x"} towards a generic result @{text "P x"}, + while coinduction introduces @{text "A x"} starting with @{text "B + x"}, for a suitable ``bisimulation'' @{text 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 ``@{text "taking: t\<^sub>1 \ t\<^sub>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 @{method + induct} and @{method 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 @{variable ?case} for + the conclusion will be provided with each case, provided that term + is fully specified. + + The @{command "print_cases"} command prints all named cases present + in the current proof state. + + \medskip Despite the additional infrastructure, both @{method cases} + and @{method 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 @{text + "\x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ \\<^sub>n \ \"} + reappears unchanged after the case split. + + The @{method 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: @{text hyps} stemming from the rule and + @{text prems} from the goal statement. This is reflected in the + extracted cases accordingly, so invoking ``@{command "case"}~@{text + c}'' will provide separate facts @{text c.hyps} and @{text c.prems}, + as well as fact @{text 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 @{text cases}, @{text induct}, or @{text coinduct} rule is + applied. +*} + + +subsection {* Declaring rules *} + +text {* + \begin{matharray}{rcl} + @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{attribute_def cases} & : & \isaratt \\ + @{attribute_def induct} & : & \isaratt \\ + @{attribute_def coinduct} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + 'cases' spec + ; + 'induct' spec + ; + 'coinduct' spec + ; + + spec: ('type' | 'pred' | 'set') ':' nameref + ; + \end{rail} + + \begin{descr} + + \item [@{command "print_induct_rules"}] prints cases and induct + rules for predicates (or sets) and types of the current context. + + \item [@{attribute cases}, @{attribute induct}, and @{attribute + 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 @{attribute + case_names} and @{attribute params} attributes to adjust names of + cases and parameters of a rule; the @{attribute consumes} + declaration is taken care of automatically: @{attribute + consumes}~@{text 0} is specified for ``type'' rules and @{attribute + consumes}~@{text 1} for ``predicate'' / ``set'' rules. + + \end{descr} +*} + end diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Jun 02 22:50:23 2008 +0200 @@ -12,22 +12,24 @@ \begin{matharray}{rcl} @{command_def "header"} & : & \isarkeep{toplevel} \\ @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\ - @{command_def "end"} & : & \isartrans{theory}{toplevel} \\ + @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\ \end{matharray} - Isabelle/Isar theories are defined via theory, which contain both - specifications and proofs; occasionally definitional mechanisms also - require some explicit proof. + Isabelle/Isar theories are defined via theory file, which contain + both specifications and proofs; occasionally definitional mechanisms + also require some explicit proof. The theory body may be + sub-structered by means of \emph{local theory} target mechanisms, + notably @{command "locale"} and @{command "class"}. The first ``real'' command of any theory has to be @{command "theory"}, which starts a new theory based on the merge of existing ones. Just preceding the @{command "theory"} keyword, there may be an optional @{command "header"} declaration, which is relevant to document preparation only; it acts very much like a special - pre-theory markup command (cf.\ \secref{sec:markup-thy} and - \secref{sec:markup-thy}). The @{command "end"} command concludes a - theory development; it has to be the very last command of any theory - file loaded in batch-mode. + pre-theory markup command (cf.\ \secref{sec:markup} and). The + @{command (global) "end"} command + concludes a theory development; it has to be the very last command + of any theory file loaded in batch-mode. \begin{rail} 'header' text @@ -44,8 +46,7 @@ markup just preceding the formal beginning of a theory. In actual document preparation the corresponding {\LaTeX} macro @{verbatim "\\isamarkupheader"} may be redefined to produce chapter or section - headings. See also \secref{sec:markup-thy} and - \secref{sec:markup-prf} for further markup commands. + headings. See also \secref{sec:markup} for further markup commands. \item [@{command "theory"}~@{text "A \ B\<^sub>1 \ B\<^sub>n \"}] starts a new theory @{text A} based on the @@ -65,10 +66,1269 @@ text (typically via explicit @{command_ref "use"} in the body text, see \secref{sec:ML}). - \item [@{command "end"}] concludes the current theory definition or - context switch. + \item [@{command (global) "end"}] concludes the current theory + definition. + + \end{descr} +*} + + +section {* Local theory targets \label{sec:target} *} + +text {* + 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 ``@{text "-"}'' signifies the + global theory context. + + \begin{matharray}{rcll} + @{command_def "context"} & : & \isartrans{theory}{local{\dsh}theory} \\ + @{command_def (local) "end"} & : & \isartrans{local{\dsh}theory}{theory} \\ + \end{matharray} + + \indexouternonterm{target} + \begin{rail} + 'context' name 'begin' + ; + + target: '(' 'in' name ')' + ; + \end{rail} + + \begin{descr} + + \item [@{command "context"}~@{text "c \"}] recommences an + existing locale or class context @{text c}. Note that locale and + class definitions allow to include the @{keyword_ref "begin"} + keyword as well, in order to continue the local theory immediately + after the initial specification. + + \item [@{command (local) "end"}] concludes the current local theory + and continues the enclosing global theory. Note that a global + @{command (global) "end"} has a different meaning: it concludes the + theory itself (\secref{sec:begin-thy}). + + \item [@{text "(\ c)"}] given after any local theory command + specifies an immediate target, e.g.\ ``@{command + "definition"}~@{text "(\ c) \"}'' or ``@{command + "theorem"}~@{text "(\ c) \"}''. This works both in a local or + global theory context; the current target context will be suspended + for this command only. Note that ``@{text "(\ -)"}'' 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 + @{text c} with parameter @{text x} and assumption @{text "A[x]"}. + + 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, + @{text "a \ t[x]"} becomes @{text "c.a ?x \ t[?x]"} at the theory + level (for arbitrary @{text "?x"}), together with a local + abbreviation @{text "c \ c.a x"} in the target context (for the + fixed parameter @{text x}). + + Theorems are exported by discharging the assumptions and + generalizing the parameters of the context. For example, @{text "a: + B[x]"} becomes @{text "c.a: A[?x] \ B[?x]"}, again for arbitrary + @{text "?x"}. +*} + + +section {* Basic specification elements *} + +text {* + \begin{matharray}{rcll} + @{command_def "axiomatization"} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ + @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\ + @{attribute_def "defn"} & : & \isaratt \\ + @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "no_notation"} & : & \isarkeep{local{\dsh}theory} \\ + \end{matharray} + + These specification mechanisms provide a slightly more abstract view + than the underlying primitives of @{command "consts"}, @{command + "defs"} (see \secref{sec:consts}), and @{command "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 [@{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m + \ \\<^sub>1 \ \\<^sub>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 [@{command "definition"}~@{text "c \ eq"}] produces an + internal definition @{text "c \ t"} according to the specification + given as @{text 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 @{attribute defn} by the + object-logic. This usually covers object-level equality @{text "x = + y"} and equivalence @{text "A \ B"}. End-users normally need not + change the @{attribute defn} setup. + + Definitions may be presented with explicit arguments on the LHS, as + well as additional conditions, e.g.\ @{text "f x y = t"} instead of + @{text "f \ \x y. t"} and @{text "y \ 0 \ g x y = u"} instead of an + unrestricted @{text "g \ \x y. u"}. + + \item [@{command "abbreviation"}~@{text "c \ eq"}] introduces + a syntactic constant which is associated with a certain term + according to the meta-level equality @{text 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 @{text mode} specification restricts output to a + particular print mode; using ``@{text input}'' here achieves the + effect of one-way abbreviations. The mode may also include an + ``@{keyword "output"}'' qualifier that affects the concrete syntax + declared for abbreviations, cf.\ @{command "syntax"} in + \secref{sec:syn-trans}. + + \item [@{command "print_abbrevs"}] prints all constant abbreviations + of the current context. + + \item [@{command "notation"}~@{text "c (mx)"}] associates mixfix + syntax with an existing constant or fixed variable. This is a + robust interface to the underlying @{command "syntax"} primitive + (\secref{sec:syn-trans}). Type declaration and internal syntactic + representation of the given entity is retrieved from the context. + + \item [@{command "no_notation"}] is similar to @{command + "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}). +*} + + +section {* Generic declarations *} + +text {* + 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} + @{command_def "declaration"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "declare"} & : & \isarkeep{local{\dsh}theory} \\ + \end{matharray} + + \begin{rail} + 'declaration' target? text + ; + 'declare' target? (thmrefs + 'and') + ; + \end{rail} + + \begin{descr} + + \item [@{command "declaration"}~@{text d}] adds the declaration + function @{text d} of ML type @{ML_type 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 [@{command "declare"}~@{text thms}] declares theorems to the + current local theory context. No theorem binding is involved here, + unlike @{command "theorems"} or @{command "lemmas"} (cf.\ + \secref{sec:axms-thms}), so @{command "declare"} only has the effect + of applying attributes as included in the theorem specification. + + \end{descr} +*} + + +section {* Locales \label{sec:locale} *} + +text {* + 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}). +*} + + +subsection {* Locale specifications *} + +text {* + \begin{matharray}{rcl} + @{command_def "locale"} & : & \isartrans{theory}{local{\dsh}theory} \\ + @{command_def "print_locale"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_locales"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{method_def intro_locales} & : & \isarmeth \\ + @{method_def unfold_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 [@{command "locale"}~@{text "loc = import + body"}] defines a + new locale @{text loc} as a context consisting of a certain view of + existing locales (@{text import}) plus some additional elements + (@{text body}). Both @{text import} and @{text body} are optional; + the degenerate form @{command "locale"}~@{text 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 @{text import} consists of a structured context expression, + consisting of references to existing locales, renamed contexts, or + merged contexts. Renaming uses positional notation: @{text "c + x\<^sub>1 \ x\<^sub>n"} means that (a prefix of) the fixed + parameters of context @{text c} are named @{text "x\<^sub>1, \, + x\<^sub>n"}; a ``@{text _}'' (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 ``@{text + "(\)"}'' (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 @{text body} consists of basic context elements, further context + expressions may be included as well. + + \begin{descr} + + \item [@{element "fixes"}~@{text "x :: \ (mx)"}] declares a local + parameter of type @{text \} and mixfix annotation @{text mx} (both + are optional). The special syntax declaration ``@{text + "(\)"}'' means that @{text x} may be referenced + implicitly in this context. + + \item [@{element "constrains"}~@{text "x :: \"}] introduces a type + constraint @{text \} on the local parameter @{text x}. + + \item [@{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"}] + introduces local premises, similar to @{command "assume"} within a + proof (cf.\ \secref{sec:proof-context}). + + \item [@{element "defines"}~@{text "a: x \ t"}] defines a previously + declared parameter. This is similar to @{command "def"} within a + proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} + takes an equational proposition instead of variable-term pair. The + left-hand side of the equation may have additional arguments, e.g.\ + ``@{element "defines"}~@{text "f x\<^sub>1 \ x\<^sub>n \ t"}''. + + \item [@{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] + reconsiders facts within a local context. Most notably, this may + include arbitrary declarations in any attribute specifications + included here, e.g.\ a local @{attribute simp} rule. + + \item [@{element "includes"}~@{text 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 @{text 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 ``@{text "(\ p\<^sub>1 \ p\<^sub>n)"}'' patterns given + in the syntax of @{element "assumes"} and @{element "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 @{text + loc_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 @{text 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 @{text \} by @{text \}, and + @{text "\"} by @{text "\"} in HOL; see also + \secref{sec:object-logic}). Separate introduction rules @{text + loc_axioms.intro} and @{text loc.intro} are provided as well. + + The @{text "(open)"} option of a locale specification prevents both + the current @{text loc_axioms} and cumulative @{text loc} predicate + constructions. Predicates are also omitted for empty specification + texts. + + \item [@{command "print_locale"}~@{text "import + body"}] prints the + specified locale expression in a flattened form. The notable + special case @{command "print_locale"}~@{text 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 @{element "notes"} elements by default. + Use @{command "print_locale"}@{text "!"} to get them included. + + \item [@{command "print_locales"}] prints the names of all locales + of the current theory. + + \item [@{method intro_locales} and @{method unfold_locales}] + repeatedly expand all introduction rules of locale predicates of the + theory. While @{method intro_locales} only applies the @{text + loc.intro} introduction rules and therefore does not decend to + assumptions, @{method unfold_locales} is more aggressive and applies + @{text loc_axioms.intro} as well. Both methods are aware of locale + specifications entailed by the context, both from target and + @{element "includes"} statements, and from interpretations (see + below). New goals that are entailed by the current context are + discharged automatically. + + \end{descr} +*} + + +subsection {* Interpretation of locales *} + +text {* + 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 @{command + "interpretation"}) and also within a proof body (command @{command + "interpret"}). + + \begin{matharray}{rcl} + @{command_def "interpretation"} & : & \isartrans{theory}{proof(prove)} \\ + @{command_def "interpret"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + @{command_def "print_interps"}@{text "\<^sup>*"} & : & \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 [@{command "interpretation"}~@{text "expr insts \ eqns"}] + + The first form of @{command "interpretation"} interprets @{text + expr} in the theory. The instantiation is given as a list of terms + @{text 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 ``@{text _}'' 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 @{keyword "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 [@{command "interpretation"}~@{text "name \ expr"}] + + This form of the command interprets @{text expr} in the locale + @{text name}. It requires a proof that the specification of @{text + name} implies the specification of @{text expr}. As in the + localized version of the theorem command, the proof is in the + context of @{text name}. After the proof obligation has been + dischared, the facts of @{text expr} become part of locale @{text + name} as \emph{derived} context elements and are available when the + context @{text name} is subsequently entered. Note that, like + import, this is dynamic: facts added to a locale part of @{text + expr} after interpretation become also available in @{text 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 ``@{text _}''). + + Unlike interpretation in theories, instantiation is confined to the + renaming of parameters, which may be specified as part of the + context expression @{text expr}. Using defined parameters in @{text + name} one may achieve an effect similar to instantiation, though. + + Only specification fragments of @{text expr} that are not already + part of @{text name} (be it imported, derived or a derived fragment + of the import) are considered by interpretation. This enables + circular interpretations. + + If interpretations of @{text name} exist in the current theory, the + command adds interpretations for @{text expr} as well, with the same + prefix and attributes, although only for fragments of @{text expr} + that are not interpreted in the theory already. + + \item [@{command "interpret"}~@{text "expr insts \ eqns"}] + interprets @{text expr} in the proof context and is otherwise + similar to interpretation in theories. + + \item [@{command "print_interps"}~@{text loc}] prints the + interpretations of a particular locale @{text 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} +*} + + +section {* Classes \label{sec:class} *} + +text {* + A class is a particular locale with \emph{exactly one} type variable + @{text \}. 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} + @{command_def "class"} & : & \isartrans{theory}{local{\dsh}theory} \\ + @{command_def "instantiation"} & : & \isartrans{theory}{local{\dsh}theory} \\ + @{command_def "instance"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ + @{command_def "subclass"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ + @{command_def "print_classes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{method_def intro_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 [@{command "class"}~@{text "c = superclasses + body"}] defines + a new class @{text c}, inheriting from @{text superclasses}. This + introduces a locale @{text c} with import of all locales @{text + superclasses}. + + Any @{element "fixes"} in @{text body} are lifted to the global + theory level (\emph{class operations} @{text "f\<^sub>1, \, + f\<^sub>n"} of class @{text c}), mapping the local type parameter + @{text \} to a schematic type variable @{text "?\ :: c"}. + + Likewise, @{element "assumes"} in @{text body} are also lifted, + mapping each local parameter @{text "f :: \[\]"} to its + corresponding global constant @{text "f :: \[?\ :: c]"}. The + corresponding introduction rule is provided as @{text + c_class_axioms.intro}. This rule should be rarely needed directly + --- the @{method intro_classes} method takes care of the details of + class membership proofs. + + \item [@{command "instantiation"}~@{text "t :: (s\<^sub>1, \, + s\<^sub>n) s \"}] opens a theory target (cf.\ + \secref{sec:target}) which allows to specify class operations @{text + "f\<^sub>1, \, f\<^sub>n"} corresponding to sort @{text s} at the + particular type instance @{text "(\\<^sub>1 :: s\<^sub>1, \, + \\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command + in the target body poses a goal stating these type arities. The + target is concluded by an @{command_ref (local) "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 [@{command "instance"}] in an instantiation target body sets + up a goal stating the type arities claimed at the opening @{command + "instantiation"}. The proof would usually proceed by @{method + intro_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 [@{command "subclass"}~@{text c}] in a class context for class + @{text d} sets up a goal stating that class @{text c} is logically + contained in class @{text d}. After finishing the proof, class + @{text d} is proven to be subclass @{text c} and the locale @{text + c} is interpreted into @{text d} simultaneously. + + \item [@{command "print_classes"}] prints all classes in the current + theory. + + \item [@{method intro_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 @{command "proof"}). In particular, + instantiation of trivial (syntactic) classes may be performed by a + single ``@{command ".."}'' proof step. \end{descr} *} + +subsection {* The class target *} + +text {* + %FIXME check + + A named context may refer to a locale (cf.\ \secref{sec:target}). + If this locale is also a class @{text c}, apart from the common + locale target behaviour the following happens. + + \begin{itemize} + + \item Local constant declarations @{text "g[\]"} referring to the + local type parameter @{text \} and local parameters @{text "f[\]"} + are accompanied by theory-level constants @{text "g[?\ :: c]"} + referring to theory-level class operations @{text "f[?\ :: c]"}. + + \item Local theorem bindings are lifted as are assumptions. + + \item Local syntax refers to local operations @{text "g[\]"} and + global operations @{text "g[?\ :: c]"} uniformly. Type inference + resolves ambiguities. In rare cases, manual type annotations are + needed. + + \end{itemize} +*} + + +section {* Axiomatic type classes \label{sec:axclass} *} + +text {* + \begin{warn} + This describes the old interface to axiomatic type-classes in + Isabelle. See \secref{sec:class} for a more recent higher-level + view on the same ideas. + \end{warn} + + \begin{matharray}{rcl} + @{command_def "axclass"} & : & \isartrans{theory}{theory} \\ + @{command_def "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 [@{command "axclass"}~@{text "c \ c\<^sub>1, \, c\<^sub>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 + @{text c_class.intro}); this rule is employed by method @{method + intro_classes} to support instantiation proofs of this class. + + The ``class axioms'' are stored as theorems according to the given + name specifications, adding @{text "c_class"} as name space prefix; + the same facts are also stored collectively as @{text + c_class.axioms}. + + \item [@{command "instance"}~@{text "c\<^sub>1 \ c\<^sub>2"} and + @{command "instance"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) s"}] + setup a goal stating a class relation or type arity. The proof + would usually proceed by @{method intro_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} +*} + + +section {* Unrestricted overloading *} + +text {* + 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 @{command "instantiation"} (see + \secref{sec:class}). Sometimes low-level overloading is desirable. + The @{command "overloading"} target provides a convenient view for + end-users. + + \begin{matharray}{rcl} + @{command_def "overloading"} & : & \isartrans{theory}{local{\dsh}theory} \\ + \end{matharray} + + \begin{rail} + 'overloading' \\ + ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' + \end{rail} + + \begin{descr} + + \item [@{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: + \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"}] + 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 @{text + "x\<^sub>i"} to constants @{text "c\<^sub>i"} at particular type + instances. The definitions themselves are established using common + specification tools, using the names @{text "x\<^sub>i"} as + reference to the corresponding constants. The target is concluded + by @{command (local) "end"}. + + A @{text "(unchecked)"} 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} +*} + + +section {* Incorporating ML code \label{sec:ML} *} + +text {* + \begin{matharray}{rcl} + @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ + @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ + @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\ + @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\ + @{command_def "setup"} & : & \isartrans{theory}{theory} \\ + @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'use' name + ; + ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text + ; + 'method\_setup' name '=' text text + ; + \end{rail} + + \begin{descr} + + \item [@{command "use"}~@{text "file"}] reads and executes ML + commands from @{text "file"}. The current theory context is passed + down to the ML toplevel and may be modified, using @{ML + "Context.>>"} or derived ML commands. The file name is checked with + the @{keyword_ref "uses"} dependency declaration given in the theory + header (see also \secref{sec:begin-thy}). + + \item [@{command "ML"}~@{text "text"}] is similar to @{command + "use"}, but executes ML commands directly from the given @{text + "text"}. + + \item [@{command "ML_val"} and @{command "ML_command"}] are + diagnostic versions of @{command "ML"}, which means that the context + may not be updated. @{command "ML_val"} echos the bindings produced + at the ML toplevel, but @{command "ML_command"} is silent. + + \item [@{command "setup"}~@{text "text"}] changes the current theory + context by applying @{text "text"}, which refers to an ML expression + of type @{ML_type "theory -> theory"}. This enables to initialize + any object-logic specific tools and packages written in ML, for + example. + + \item [@{command "method_setup"}~@{text "name = text description"}] + defines a proof method in the current theory. The given @{text + "text"} has to be an ML expression of type @{ML_type "Args.src -> + Proof.context -> Proof.method"}. Parsing concrete method syntax + from @{ML_type Args.src} input can be quite tedious in general. The + following simple examples are for methods without any explicit + arguments, or a list of theorems, respectively. + +%FIXME proper antiquotations +{\footnotesize +\begin{verbatim} + Method.no_args (Method.METHOD (fn facts => foobar_tac)) + Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) + Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) + Method.thms_ctxt_args (fn thms => fn ctxt => + Method.METHOD (fn facts => foobar_tac)) +\end{verbatim} +} + + Note that mere tactic emulations may ignore the @{text facts} + parameter above. Proper proof methods would do something + appropriate with the list of current facts, though. Single-rule + methods usually do strict forward-chaining (e.g.\ by using @{ML + Drule.multi_resolves}), while automatic ones just insert the facts + using @{ML Method.insert_tac} before applying the main tactic. + + \end{descr} +*} + + +section {* Primitive specification elements *} + +subsection {* Type classes and sorts \label{sec:classes} *} + +text {* + \begin{matharray}{rcll} + @{command_def "classes"} & : & \isartrans{theory}{theory} \\ + @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\ + @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + \begin{rail} + 'classes' (classdecl +) + ; + 'classrel' (nameref ('<' | subseteq) nameref + 'and') + ; + 'defaultsort' sort + ; + \end{rail} + + \begin{descr} + + \item [@{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"}] + declares class @{text c} to be a subclass of existing classes @{text + "c\<^sub>1, \, c\<^sub>n"}. Cyclic class structures are not permitted. + + \item [@{command "classrel"}~@{text "c\<^sub>1 \ c\<^sub>2"}] states + subclass relations between existing classes @{text "c\<^sub>1"} and + @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref + "instance"} command (see \secref{sec:axclass}) provides a way to + introduce proven class relations. + + \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the + new default sort for any type variables given without sort + constraints. Usually, the default sort would be only changed when + defining a new object-logic. + + \item [@{command "class_deps"}] visualizes the subclass relation, + using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \end{descr} +*} + + +subsection {* Types and type abbreviations \label{sec:types-pure} *} + +text {* + \begin{matharray}{rcll} + @{command_def "types"} & : & \isartrans{theory}{theory} \\ + @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\ + @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\ + @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + \end{matharray} + + \begin{rail} + 'types' (typespec '=' type infix? +) + ; + 'typedecl' typespec infix? + ; + 'nonterminals' (name +) + ; + 'arities' (nameref '::' arity +) + ; + \end{rail} + + \begin{descr} + + \item [@{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"}] + introduces \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} + for existing type @{text "\"}. Unlike actual type definitions, as + are available in Isabelle/HOL for example, type synonyms are just + purely syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. + + \item [@{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"}] + declares a new type constructor @{text t}, intended as an actual + logical type (of the object-logic, if available). + + \item [@{command "nonterminals"}~@{text c}] declares type + constructors @{text c} (without arguments) to act as purely + syntactic types, i.e.\ nonterminal symbols of Isabelle's inner + syntax of terms or types. + + \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) + s"}] augments Isabelle's order-sorted signature of types by new type + constructor arities. This is done axiomatically! The @{command_ref + "instance"} command (see \S\ref{sec:axclass}) provides a way to + introduce proven type arities. + + \end{descr} +*} + + +subsection {* Constants and definitions \label{sec:consts} *} + +text {* + Definitions essentially express abbreviations within the logic. The + simplest form of a definition is @{text "c :: \ \ t"}, where @{text + c} is a newly declared constant. Isabelle also allows derived forms + where the arguments of @{text c} appear on the left, abbreviating a + prefix of @{text \}-abstractions, e.g.\ @{text "c \ \x y. t"} may be + written more conveniently as @{text "c x y \ t"}. Moreover, + definitions may be weakened by adding arbitrary pre-conditions: + @{text "A \ c x y \ t"}. + + \medskip The built-in well-formedness conditions for definitional + specifications are: + + \begin{itemize} + + \item Arguments (on the left-hand side) must be distinct variables. + + \item All variables on the right-hand side must also appear on the + left-hand side. + + \item All type variables on the right-hand side must also appear on + the left-hand side; this prohibits @{text "0 :: nat \ length ([] :: + \ list)"} for example. + + \item The definition must not be recursive. Most object-logics + provide definitional principles that can be used to express + recursion safely. + + \end{itemize} + + Overloading means that a constant being declared as @{text "c :: \ + decl"} may be defined separately on type instances @{text "c :: + (\\<^sub>1, \, \\<^sub>n) t decl"} for each type constructor @{text + t}. The right-hand side may mention overloaded constants + recursively at type instances corresponding to the immediate + argument types @{text "\\<^sub>1, \, \\<^sub>n"}. Incomplete + specification patterns impose global constraints on all occurrences, + e.g.\ @{text "d :: \ \ \"} on the left-hand side means that all + corresponding occurrences on some right-hand side need to be an + instance of this, general @{text "d :: \ \ \"} will be disallowed. + + \begin{matharray}{rcl} + @{command_def "consts"} & : & \isartrans{theory}{theory} \\ + @{command_def "defs"} & : & \isartrans{theory}{theory} \\ + @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'consts' ((name '::' type mixfix?) +) + ; + 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) + ; + \end{rail} + + \begin{rail} + 'constdefs' structs? (constdecl? constdef +) + ; + + structs: '(' 'structure' (vars + 'and') ')' + ; + constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' + ; + constdef: thmdecl? prop + ; + \end{rail} + + \begin{descr} + + \item [@{command "consts"}~@{text "c :: \"}] declares constant + @{text c} to have any instance of type scheme @{text \}. The + optional mixfix annotations may attach concrete syntax to the + constants declared. + + \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn} + as a definitional axiom for some existing constant. + + The @{text "(unchecked)"} option disables global dependency checks + for this definition, which is occasionally useful for exotic + overloading. It is at the discretion of the user to avoid malformed + theory specifications! + + The @{text "(overloaded)"} option declares definitions to be + potentially overloaded. Unless this option is given, a warning + message would be issued for any definitional equation with a more + special type than that of the corresponding constant declaration. + + \item [@{command "constdefs"}] provides a streamlined combination of + constants declarations and definitions: type-inference takes care of + the most general typing of the given specification (the optional + type constraint may refer to type-inference dummies ``@{text + _}'' as usual). The resulting type declaration needs to agree with + that of the specification; overloading is \emph{not} supported here! + + The constant name may be omitted altogether, if neither type nor + syntax declarations are given. The canonical name of the + definitional axiom for constant @{text c} will be @{text c_def}, + unless specified otherwise. Also note that the given list of + specifications is processed in a strictly sequential manner, with + type-checking being performed independently. + + An optional initial context of @{text "(structure)"} declarations + admits use of indexed syntax, using the special symbol @{verbatim + "\"} (printed as ``@{text "\"}''). The latter concept is + particularly useful with locales (see also \S\ref{sec:locale}). + + \end{descr} +*} + + +section {* Axioms and theorems \label{sec:axms-thms} *} + +text {* + \begin{matharray}{rcll} + @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\ + \end{matharray} + + \begin{rail} + 'axioms' (axmdecl prop +) + ; + ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') + ; + \end{rail} + + \begin{descr} + + \item [@{command "axioms"}~@{text "a: \"}] introduces arbitrary + statements as axioms of the meta-logic. In fact, axioms are + ``axiomatic theorems'', and may be referred later just as any other + theorem. + + Axioms are usually only introduced when declaring new logical + systems. Everyday work is typically done the hard way, with proper + definitions and proven theorems. + + \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] + retrieves and stores existing facts in the theory context, or the + specified target context (see also \secref{sec:target}). Typical + applications would also involve attributes, to declare Simplifier + rules, for example. + + \item [@{command "theorems"}] is essentially the same as @{command + "lemmas"}, but marks the result as a different kind of facts. + + \end{descr} +*} + + +section {* Oracles *} + +text {* + \begin{matharray}{rcl} + @{command_def "oracle"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + The oracle interface promotes a given ML function @{ML_text + "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some + type @{ML_text T} given by the user. This acts like an infinitary + specification of axioms -- there is no internal check of the + correctness of the results! The inference kernel records oracle + invocations within the internal derivation object of theorems, and + the pretty printer attaches ``@{text "[!]"}'' to indicate results + that are not fully checked by Isabelle inferences. + + \begin{rail} + 'oracle' name '(' type ')' '=' text + ; + \end{rail} + + \begin{descr} + + \item [@{command "oracle"}~@{text "name (type) = text"}] turns the + given ML expression @{text "text"} of type + @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an + ML function of type + @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is + bound to the global identifier @{ML_text name}. + + \end{descr} +*} + + +section {* Name spaces *} + +text {* + \begin{matharray}{rcl} + @{command_def "global"} & : & \isartrans{theory}{theory} \\ + @{command_def "local"} & : & \isartrans{theory}{theory} \\ + @{command_def "hide"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'hide' ('(open)')? name (nameref + ) + ; + \end{rail} + + Isabelle organizes any kind of name declarations (of types, + constants, theorems etc.) by separate hierarchically structured name + spaces. Normally the user does not have to control the behavior of + name spaces by hand, yet the following commands provide some way to + do so. + + \begin{descr} + + \item [@{command "global"} and @{command "local"}] change the + current name declaration mode. Initially, theories start in + @{command "local"} mode, causing all names to be automatically + qualified by the theory name. Changing this to @{command "global"} + causes all names to be declared without the theory prefix, until + @{command "local"} is declared again. + + Note that global names are prone to get hidden accidently later, + when qualified names of the same base name are introduced. + + \item [@{command "hide"}~@{text "space names"}] fully removes + declarations from a given name space (which may be @{text "class"}, + @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text + "(open)"} option, only the base name is hidden. Global + (unqualified) names may never be hidden. + + Note that hiding name space accesses has no impact on logical + declarations -- they remain valid internally. Entities that are no + longer accessible to the user are printed with the special qualifier + ``@{text "??"}'' prefixed to the full internal name. + + \end{descr} +*} + + +section {* Syntax and translations \label{sec:syn-trans} *} + +text {* + \begin{matharray}{rcl} + @{command_def "syntax"} & : & \isartrans{theory}{theory} \\ + @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\ + @{command_def "translations"} & : & \isartrans{theory}{theory} \\ + @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + ('syntax' | 'no\_syntax') mode? (constdecl +) + ; + ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) + ; + + mode: ('(' ( name | 'output' | name 'output' ) ')') + ; + transpat: ('(' nameref ')')? string + ; + \end{rail} + + \begin{descr} + + \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to + @{command "consts"}~@{text decls}, except that the actual logical + signature extension is omitted. Thus the context free grammar of + Isabelle's inner syntax may be augmented in arbitrary ways, + independently of the logic. The @{text mode} argument refers to the + print mode that the grammar rules belong; unless the @{keyword_ref + "output"} indicator is given, all productions are added both to the + input and output grammar. + + \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes + grammar declarations (and translations) resulting from @{text + decls}, which are interpreted in the same manner as for @{command + "syntax"} above. + + \item [@{command "translations"}~@{text rules}] specifies syntactic + translation rules (i.e.\ macros): parse~/ print rules (@{text "\"}), + parse rules (@{text "\"}), or print rules (@{text "\"}). + Translation patterns may be prefixed by the syntactic category to be + used for parsing; the default is @{text logic}. + + \item [@{command "no_translations"}~@{text rules}] removes syntactic + translation rules, which are interpreted in the same manner as for + @{command "translations"} above. + + \end{descr} +*} + + +section {* Syntax translation functions *} + +text {* + \begin{matharray}{rcl} + @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | + 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text + ; + + 'token\_translation' text + ; + \end{rail} + + Syntax translation functions written in ML admit almost arbitrary + manipulations of Isabelle's inner syntax. Any of the above commands + have a single \railqtok{text} argument that refers to an ML + expression of appropriate type, which are as follows by default: + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation : (string * (ast list -> ast)) list +val parse_translation : (string * (term list -> term)) list +val print_translation : (string * (term list -> term)) list +val typed_print_translation : + (string * (bool -> typ -> term list -> term)) list +val print_ast_translation : (string * (ast list -> ast)) list +val token_translation : + (string * string * (string -> string * real)) list +\end{ttbox} + + If the @{text "(advanced)"} option is given, the corresponding + translation functions may depend on the current theory or proof + context. This allows to implement advanced syntax mechanisms, as + translations functions may refer to specific theory declarations or + auxiliary proof data. + + See also \cite[\S8]{isabelle-ref} for more information on the + general concept of syntax transformations in Isabelle. + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation: + (string * (Context.generic -> ast list -> ast)) list +val parse_translation: + (string * (Context.generic -> term list -> term)) list +val print_translation: + (string * (Context.generic -> term list -> term)) list +val typed_print_translation: + (string * (Context.generic -> bool -> typ -> term list -> term)) list +val print_ast_translation: + (string * (Context.generic -> ast list -> ast)) list +\end{ttbox} +*} + end diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/pure.thy --- a/doc-src/IsarRef/Thy/pure.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/pure.thy Mon Jun 02 22:50:23 2008 +0200 @@ -6,629 +6,6 @@ chapter {* Basic language elements \label{ch:pure-syntax} *} -text {* - Subsequently, we introduce the main part of Pure theory and proof - commands, together with fundamental proof methods and attributes. - \Chref{ch:gen-tools} describes further Isar elements provided by - generic tools and packages (such as the Simplifier) that are either - part of Pure Isabelle or pre-installed in most object logics. - Specific language elements introduced by the major object-logics are - described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf} - (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless, - examples given in the generic parts will usually refer to - Isabelle/HOL as well. - - \medskip Isar commands may be either \emph{proper} document - constructors, or \emph{improper commands}. Some proof methods and - attributes introduced later are classified as improper as well. - Improper Isar language elements, which are subsequently marked by - ``@{text "\<^sup>*"}'', are often helpful when developing proof - documents, while their use is discouraged for the final - human-readable outcome. Typical examples are diagnostic commands - that print terms or theorems according to the current context; other - commands emulate old-style tactical theorem proving. -*} - - -section {* Theory commands *} - -subsection {* Markup commands \label{sec:markup-thy} *} - -text {* - \begin{matharray}{rcl} - @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\ - \end{matharray} - - Apart from formal comments (see \secref{sec:comments}), markup - commands provide a structured way to insert text into the document - generated from a theory (see \cite{isabelle-sys} for more - information on Isabelle's document preparation tools). - - \begin{rail} - ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text - ; - 'text\_raw' text - ; - \end{rail} - - \begin{descr} - - \item [@{command "chapter"}, @{command "section"}, @{command - "subsection"}, and @{command "subsubsection"}] mark chapter and - section headings. - - \item [@{command "text"}] specifies paragraphs of plain text. - - \item [@{command "text_raw"}] inserts {\LaTeX} source into the - output, without additional markup. Thus the full range of document - manipulations becomes available. - - \end{descr} - - The @{text "text"} argument of these markup commands (except for - @{command "text_raw"}) may contain references to formal entities - (``antiquotations'', see also \secref{sec:antiq}). These are - interpreted in the present theory context, or the named @{text - "target"}. - - Any of these markup elements corresponds to a {\LaTeX} command with - the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning - commands this is a plain macro with a single argument, e.g.\ - @{verbatim "\\isamarkupchapter{"}@{text "\"}@{verbatim "}"} for - @{command "chapter"}. The @{command "text"} markup results in a - {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text - "\"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"} - causes the text to be inserted directly into the {\LaTeX} source. - - \medskip Additional markup commands are available for proofs (see - \secref{sec:markup-prf}). Also note that the @{command_ref - "header"} declaration (see \secref{sec:begin-thy}) admits to insert - section markup just preceding the actual theory definition. -*} - - -subsection {* Type classes and sorts \label{sec:classes} *} - -text {* - \begin{matharray}{rcll} - @{command_def "classes"} & : & \isartrans{theory}{theory} \\ - @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\ - @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\ - \end{matharray} - - \begin{rail} - 'classes' (classdecl +) - ; - 'classrel' (nameref ('<' | subseteq) nameref + 'and') - ; - 'defaultsort' sort - ; - \end{rail} - - \begin{descr} - - \item [@{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"}] - declares class @{text c} to be a subclass of existing classes @{text - "c\<^sub>1, \, c\<^sub>n"}. Cyclic class structures are not permitted. - - \item [@{command "classrel"}~@{text "c\<^sub>1 \ c\<^sub>2"}] states - subclass relations between existing classes @{text "c\<^sub>1"} and - @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref - "instance"} command (see \secref{sec:axclass}) provides a way to - introduce proven class relations. - - \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the - new default sort for any type variables given without sort - constraints. Usually, the default sort would be only changed when - defining a new object-logic. - - \item [@{command "class_deps"}] visualizes the subclass relation, - using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - - \end{descr} -*} - - -subsection {* Primitive types and type abbreviations \label{sec:types-pure} *} - -text {* - \begin{matharray}{rcll} - @{command_def "types"} & : & \isartrans{theory}{theory} \\ - @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\ - @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\ - @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - \end{matharray} - - \begin{rail} - 'types' (typespec '=' type infix? +) - ; - 'typedecl' typespec infix? - ; - 'nonterminals' (name +) - ; - 'arities' (nameref '::' arity +) - ; - \end{rail} - - \begin{descr} - - \item [@{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"}] - introduces \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} - for existing type @{text "\"}. Unlike actual type definitions, as - are available in Isabelle/HOL for example, type synonyms are just - purely syntactic abbreviations without any logical significance. - Internally, type synonyms are fully expanded. - - \item [@{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"}] - declares a new type constructor @{text t}, intended as an actual - logical type (of the object-logic, if available). - - \item [@{command "nonterminals"}~@{text c}] declares type - constructors @{text c} (without arguments) to act as purely - syntactic types, i.e.\ nonterminal symbols of Isabelle's inner - syntax of terms or types. - - \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) - s"}] augments Isabelle's order-sorted signature of types by new type - constructor arities. This is done axiomatically! The @{command_ref - "instance"} command (see \S\ref{sec:axclass}) provides a way to - introduce proven type arities. - - \end{descr} -*} - - -subsection {* Primitive constants and definitions \label{sec:consts} *} - -text {* - Definitions essentially express abbreviations within the logic. The - simplest form of a definition is @{text "c :: \ \ t"}, where @{text - c} is a newly declared constant. Isabelle also allows derived forms - where the arguments of @{text c} appear on the left, abbreviating a - prefix of @{text \}-abstractions, e.g.\ @{text "c \ \x y. t"} may be - written more conveniently as @{text "c x y \ t"}. Moreover, - definitions may be weakened by adding arbitrary pre-conditions: - @{text "A \ c x y \ t"}. - - \medskip The built-in well-formedness conditions for definitional - specifications are: - - \begin{itemize} - - \item Arguments (on the left-hand side) must be distinct variables. - - \item All variables on the right-hand side must also appear on the - left-hand side. - - \item All type variables on the right-hand side must also appear on - the left-hand side; this prohibits @{text "0 :: nat \ length ([] :: - \ list)"} for example. - - \item The definition must not be recursive. Most object-logics - provide definitional principles that can be used to express - recursion safely. - - \end{itemize} - - Overloading means that a constant being declared as @{text "c :: \ - decl"} may be defined separately on type instances @{text "c :: - (\\<^sub>1, \, \\<^sub>n) t decl"} for each type constructor @{text - t}. The right-hand side may mention overloaded constants - recursively at type instances corresponding to the immediate - argument types @{text "\\<^sub>1, \, \\<^sub>n"}. Incomplete - specification patterns impose global constraints on all occurrences, - e.g.\ @{text "d :: \ \ \"} on the left-hand side means that all - corresponding occurrences on some right-hand side need to be an - instance of this, general @{text "d :: \ \ \"} will be disallowed. - - \begin{matharray}{rcl} - @{command_def "consts"} & : & \isartrans{theory}{theory} \\ - @{command_def "defs"} & : & \isartrans{theory}{theory} \\ - @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - 'consts' ((name '::' type mixfix?) +) - ; - 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) - ; - \end{rail} - - \begin{rail} - 'constdefs' structs? (constdecl? constdef +) - ; - - structs: '(' 'structure' (vars + 'and') ')' - ; - constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' - ; - constdef: thmdecl? prop - ; - \end{rail} - - \begin{descr} - - \item [@{command "consts"}~@{text "c :: \"}] declares constant - @{text c} to have any instance of type scheme @{text \}. The - optional mixfix annotations may attach concrete syntax to the - constants declared. - - \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn} - as a definitional axiom for some existing constant. - - The @{text "(unchecked)"} option disables global dependency checks - for this definition, which is occasionally useful for exotic - overloading. It is at the discretion of the user to avoid malformed - theory specifications! - - The @{text "(overloaded)"} option declares definitions to be - potentially overloaded. Unless this option is given, a warning - message would be issued for any definitional equation with a more - special type than that of the corresponding constant declaration. - - \item [@{command "constdefs"}] provides a streamlined combination of - constants declarations and definitions: type-inference takes care of - the most general typing of the given specification (the optional - type constraint may refer to type-inference dummies ``@{text - _}'' as usual). The resulting type declaration needs to agree with - that of the specification; overloading is \emph{not} supported here! - - The constant name may be omitted altogether, if neither type nor - syntax declarations are given. The canonical name of the - definitional axiom for constant @{text c} will be @{text c_def}, - unless specified otherwise. Also note that the given list of - specifications is processed in a strictly sequential manner, with - type-checking being performed independently. - - An optional initial context of @{text "(structure)"} declarations - admits use of indexed syntax, using the special symbol @{verbatim - "\"} (printed as ``@{text "\"}''). The latter concept is - particularly useful with locales (see also \S\ref{sec:locale}). - - \end{descr} -*} - - -subsection {* Syntax and translations \label{sec:syn-trans} *} - -text {* - \begin{matharray}{rcl} - @{command_def "syntax"} & : & \isartrans{theory}{theory} \\ - @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\ - @{command_def "translations"} & : & \isartrans{theory}{theory} \\ - @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - ('syntax' | 'no\_syntax') mode? (constdecl +) - ; - ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) - ; - - mode: ('(' ( name | 'output' | name 'output' ) ')') - ; - transpat: ('(' nameref ')')? string - ; - \end{rail} - - \begin{descr} - - \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to - @{command "consts"}~@{text decls}, except that the actual logical - signature extension is omitted. Thus the context free grammar of - Isabelle's inner syntax may be augmented in arbitrary ways, - independently of the logic. The @{text mode} argument refers to the - print mode that the grammar rules belong; unless the @{keyword_ref - "output"} indicator is given, all productions are added both to the - input and output grammar. - - \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes - grammar declarations (and translations) resulting from @{text - decls}, which are interpreted in the same manner as for @{command - "syntax"} above. - - \item [@{command "translations"}~@{text rules}] specifies syntactic - translation rules (i.e.\ macros): parse~/ print rules (@{text "\"}), - parse rules (@{text "\"}), or print rules (@{text "\"}). - Translation patterns may be prefixed by the syntactic category to be - used for parsing; the default is @{text logic}. - - \item [@{command "no_translations"}~@{text rules}] removes syntactic - translation rules, which are interpreted in the same manner as for - @{command "translations"} above. - - \end{descr} -*} - - -subsection {* Axioms and theorems \label{sec:axms-thms} *} - -text {* - \begin{matharray}{rcll} - @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\ - \end{matharray} - - \begin{rail} - 'axioms' (axmdecl prop +) - ; - ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') - ; - \end{rail} - - \begin{descr} - - \item [@{command "axioms"}~@{text "a: \"}] introduces arbitrary - statements as axioms of the meta-logic. In fact, axioms are - ``axiomatic theorems'', and may be referred later just as any other - theorem. - - Axioms are usually only introduced when declaring new logical - systems. Everyday work is typically done the hard way, with proper - definitions and proven theorems. - - \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] - retrieves and stores existing facts in the theory context, or the - specified target context (see also \secref{sec:target}). Typical - applications would also involve attributes, to declare Simplifier - rules, for example. - - \item [@{command "theorems"}] is essentially the same as @{command - "lemmas"}, but marks the result as a different kind of facts. - - \end{descr} -*} - - -subsection {* Name spaces *} - -text {* - \begin{matharray}{rcl} - @{command_def "global"} & : & \isartrans{theory}{theory} \\ - @{command_def "local"} & : & \isartrans{theory}{theory} \\ - @{command_def "hide"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - 'hide' ('(open)')? name (nameref + ) - ; - \end{rail} - - Isabelle organizes any kind of name declarations (of types, - constants, theorems etc.) by separate hierarchically structured name - spaces. Normally the user does not have to control the behavior of - name spaces by hand, yet the following commands provide some way to - do so. - - \begin{descr} - - \item [@{command "global"} and @{command "local"}] change the - current name declaration mode. Initially, theories start in - @{command "local"} mode, causing all names to be automatically - qualified by the theory name. Changing this to @{command "global"} - causes all names to be declared without the theory prefix, until - @{command "local"} is declared again. - - Note that global names are prone to get hidden accidently later, - when qualified names of the same base name are introduced. - - \item [@{command "hide"}~@{text "space names"}] fully removes - declarations from a given name space (which may be @{text "class"}, - @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text - "(open)"} option, only the base name is hidden. Global - (unqualified) names may never be hidden. - - Note that hiding name space accesses has no impact on logical - declarations -- they remain valid internally. Entities that are no - longer accessible to the user are printed with the special qualifier - ``@{text "??"}'' prefixed to the full internal name. - - \end{descr} -*} - - -subsection {* Incorporating ML code \label{sec:ML} *} - -text {* - \begin{matharray}{rcl} - @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ - @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ - @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\ - @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\ - @{command_def "setup"} & : & \isartrans{theory}{theory} \\ - @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - 'use' name - ; - ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text - ; - 'method\_setup' name '=' text text - ; - \end{rail} - - \begin{descr} - - \item [@{command "use"}~@{text "file"}] reads and executes ML - commands from @{text "file"}. The current theory context is passed - down to the ML toplevel and may be modified, using @{ML - "Context.>>"} or derived ML commands. The file name is checked with - the @{keyword_ref "uses"} dependency declaration given in the theory - header (see also \secref{sec:begin-thy}). - - \item [@{command "ML"}~@{text "text"}] is similar to @{command - "use"}, but executes ML commands directly from the given @{text - "text"}. - - \item [@{command "ML_val"} and @{command "ML_command"}] are - diagnostic versions of @{command "ML"}, which means that the context - may not be updated. @{command "ML_val"} echos the bindings produced - at the ML toplevel, but @{command "ML_command"} is silent. - - \item [@{command "setup"}~@{text "text"}] changes the current theory - context by applying @{text "text"}, which refers to an ML expression - of type @{ML_type "theory -> theory"}. This enables to initialize - any object-logic specific tools and packages written in ML, for - example. - - \item [@{command "method_setup"}~@{text "name = text description"}] - defines a proof method in the current theory. The given @{text - "text"} has to be an ML expression of type @{ML_type "Args.src -> - Proof.context -> Proof.method"}. Parsing concrete method syntax - from @{ML_type Args.src} input can be quite tedious in general. The - following simple examples are for methods without any explicit - arguments, or a list of theorems, respectively. - -%FIXME proper antiquotations -{\footnotesize -\begin{verbatim} - Method.no_args (Method.METHOD (fn facts => foobar_tac)) - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) - Method.thms_ctxt_args (fn thms => fn ctxt => - Method.METHOD (fn facts => foobar_tac)) -\end{verbatim} -} - - Note that mere tactic emulations may ignore the @{text facts} - parameter above. Proper proof methods would do something - appropriate with the list of current facts, though. Single-rule - methods usually do strict forward-chaining (e.g.\ by using @{ML - Drule.multi_resolves}), while automatic ones just insert the facts - using @{ML Method.insert_tac} before applying the main tactic. - - \end{descr} -*} - - -subsection {* Syntax translation functions *} - -text {* - \begin{matharray}{rcl} - @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | - 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text - ; - - 'token\_translation' text - ; - \end{rail} - - Syntax translation functions written in ML admit almost arbitrary - manipulations of Isabelle's inner syntax. Any of the above commands - have a single \railqtok{text} argument that refers to an ML - expression of appropriate type, which are as follows by default: - -%FIXME proper antiquotations -\begin{ttbox} -val parse_ast_translation : (string * (ast list -> ast)) list -val parse_translation : (string * (term list -> term)) list -val print_translation : (string * (term list -> term)) list -val typed_print_translation : - (string * (bool -> typ -> term list -> term)) list -val print_ast_translation : (string * (ast list -> ast)) list -val token_translation : - (string * string * (string -> string * real)) list -\end{ttbox} - - If the @{text "(advanced)"} option is given, the corresponding - translation functions may depend on the current theory or proof - context. This allows to implement advanced syntax mechanisms, as - translations functions may refer to specific theory declarations or - auxiliary proof data. - - See also \cite[\S8]{isabelle-ref} for more information on the - general concept of syntax transformations in Isabelle. - -%FIXME proper antiquotations -\begin{ttbox} -val parse_ast_translation: - (string * (Context.generic -> ast list -> ast)) list -val parse_translation: - (string * (Context.generic -> term list -> term)) list -val print_translation: - (string * (Context.generic -> term list -> term)) list -val typed_print_translation: - (string * (Context.generic -> bool -> typ -> term list -> term)) list -val print_ast_translation: - (string * (Context.generic -> ast list -> ast)) list -\end{ttbox} -*} - - -subsection {* Oracles *} - -text {* - \begin{matharray}{rcl} - @{command_def "oracle"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - The oracle interface promotes a given ML function @{ML_text - "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some - type @{ML_text T} given by the user. This acts like an infinitary - specification of axioms -- there is no internal check of the - correctness of the results! The inference kernel records oracle - invocations within the internal derivation object of theorems, and - the pretty printer attaches ``@{text "[!]"}'' to indicate results - that are not fully checked by Isabelle inferences. - - \begin{rail} - 'oracle' name '(' type ')' '=' text - ; - \end{rail} - - \begin{descr} - - \item [@{command "oracle"}~@{text "name (type) = text"}] turns the - given ML expression @{text "text"} of type - @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an - ML function of type - @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is - bound to the global identifier @{ML_text name}. - - \end{descr} -*} - - -section {* Proof commands *} - -subsection {* Markup commands \label{sec:markup-prf} *} - -text {* - \begin{matharray}{rcl} - @{command_def "sect"} & : & \isartrans{proof}{proof} \\ - @{command_def "subsect"} & : & \isartrans{proof}{proof} \\ - @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\ - @{command_def "txt"} & : & \isartrans{proof}{proof} \\ - @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\ - \end{matharray} - - These markup commands for proof mode closely correspond to the ones - of theory mode (see \S\ref{sec:markup-thy}). - - \begin{rail} - ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text - ; - \end{rail} -*} - - section {* Other commands *} subsection {* Diagnostics *} @@ -846,15 +223,11 @@ @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ \end{matharray} \begin{rail} ('cd' | 'use\_thy' | 'update\_thy') name ; - ('display\_drafts' | 'print\_drafts') (name +) - ; \end{rail} \begin{descr} @@ -868,12 +241,6 @@ These system commands are scarcely used when working interactively, since loading of theories is done automatically as required. - \item [@{command "display_drafts"}~@{text paths} and @{command - "print_drafts"}~@{text paths}] perform simple output of a given list - of raw source files. Only those symbols that do not require - additional {\LaTeX} packages are displayed properly, everything else - is left verbatim. - \end{descr} *}