--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Jun 02 22:50:29 2008 +0200
@@ -0,0 +1,454 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Document{\isacharunderscore}Preparation}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Document{\isacharunderscore}Preparation\isanewline
+\isakeyword{imports}\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Document preparation \label{ch:document-prep}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+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 \verb|mkdir| and \verb|make|
+ tools. First invoke
+\begin{ttbox}
+ isatool mkdir Foo
+\end{ttbox}
+ to initialize a separate directory for session \verb|Foo| ---
+ it is safe to experiment, since \verb|isatool mkdir| never
+ overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
+ holds ML commands to load all theories required for this session;
+ furthermore \verb|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 \verb|IsaMakefile|
+ (with crude source dependencies by default). This file is located
+ one level up from the \verb|Foo| directory location. Now
+ invoke
+\begin{ttbox}
+ isatool make Foo
+\end{ttbox}
+ to run the \verb|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
+ \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
+ verbose mode.
+
+ \medskip You may also consider to tune the \verb|usedir|
+ options in \verb|IsaMakefile|, for example to change the output
+ format from \verb|pdf| to \verb|dvi|, or activate the
+ \verb|-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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Markup commands \label{sec:markup}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\[0.5ex]
+ \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\
+ \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' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}] mark chapter and
+ section headings.
+
+ \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}] specify paragraphs of
+ plain text.
+
+ \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}] insert
+ {\LaTeX} source into the output, without additional markup. Thus
+ the full range of document manipulations becomes available.
+
+ \end{descr}
+
+ The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
+ \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
+ (``antiquotations'', see also \secref{sec:antiq}). These are
+ interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
+
+ Any of these markup elements corresponds to a {\LaTeX} command with
+ the name prefixed by \verb|\isamarkup|. For the sectioning
+ commands this is a plain macro with a single argument, e.g.\
+ \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
+ \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}. The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a
+ {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}
+ causes the text to be inserted directly into the {\LaTeX} source.
+
+ \medskip The proof markup commands closely resemble those for theory
+ specifications, but have a different formal status and produce
+ different {\LaTeX} macros. Also note that the \indexref{}{command}{header}\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration (see \secref{sec:begin-thy}) admits to insert
+ section markup just preceding the actual theory definition.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Antiquotations \label{sec:antiq}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}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
+ \chref{ch:document-prep}).
+
+ Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
+ 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,
+ \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ sym\ {\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}{\isacharbraceright}{\isachardoublequote}} 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 \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| or verbatim
+ text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
+
+ \begin{descr}
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}}] prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
+ guaranteed to refer to a valid ancestor theory in the current
+ context.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
+ \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
+ may be included as well (see also \secref{sec:syn-att}); the
+ \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
+ be particularly useful to suppress printing of schematic variables.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant
+ \isa{{\isachardoublequote}c{\isachardoublequote}}.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints a constant
+ abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in
+ the current context.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}}] prints the type of a well-typed term
+ \isa{{\isachardoublequote}t{\isachardoublequote}}.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}}] prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}}] prints theorem \isa{a},
+ previously applying a style \isa{s} to it (see below).
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{t} after applying a style \isa{s} to it (see below).
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}}] prints uninterpreted source text \isa{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 [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}] 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 [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}}] is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
+ does not print the main goal.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints the (compact)
+ proof terms corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. 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 [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] is like \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}, but displays the full proof terms,
+ i.e.\ also displays information omitted in the compact proof term,
+ which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
+
+ \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}{\isachardoublequote}}] check text \isa{s} as ML value, type, and
+ structure, respectively. The source is displayed verbatim.
+
+ \end{descr}
+
+ \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
+
+ \begin{descr}
+
+ \item [\isa{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 [\isa{rhs}] is like \isa{lhs}, but extracts the second
+ argument.
+
+ \item [\isa{{\isachardoublequote}concl{\isachardoublequote}}] extracts the conclusion \isa{C} from a rule
+ in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
+
+ \item [\isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}}] extract premise
+ number \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in
+ Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
+
+ \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[\isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}]
+ control printing of explicit type and sort constraints.
+
+ \item[\isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}}] controls printing of implicit
+ structures.
+
+ \item[\isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
+ constants etc.\ to be printed in their fully qualified internal
+ form.
+
+ \item[\isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] 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[\isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] determines whether the printed
+ version of qualified names should be made sufficiently long to avoid
+ overlap with names declared further back. Set to \isa{false} for
+ more concise output.
+
+ \item[\isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}}] prints terms in \isa{{\isasymeta}}-contracted form.
+
+ \item[\isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}}] 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[\isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}}] controls line breaks in non-display
+ material.
+
+ \item[\isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the output should be
+ enclosed in double quotes.
+
+ \item[\isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}}] adds \isa{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 \isa{latex} and \isa{xsymbols}.
+
+ \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the
+ margin or indentation for pretty printing of display material.
+
+ \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the
+ antiquotation arguments, rather than the actual value. Note that
+ this does not affect well-formedness checks of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. (only the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation admits arbitrary output).
+
+ \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of
+ goals to be printed.
+
+ \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale
+ context used for evaluating and printing the subsequent argument.
+
+ \end{descr}
+
+ For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
+ ``\isa{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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Tagged commands \label{sec:tags}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Each Isabelle/Isar command may be decorated by presentation tags:
+
+ \indexouternonterm{tags}
+ \begin{rail}
+ tags: ( tag * )
+ ;
+ tag: '\%' (ident | string)
+ \end{rail}
+
+ The tags \isa{{\isachardoublequote}theory{\isachardoublequote}}, \isa{{\isachardoublequote}proof{\isachardoublequote}}, \isa{{\isachardoublequote}ML{\isachardoublequote}} are already
+ pre-declared for certain classes of commands:
+
+ \medskip
+
+ \begin{tabular}{ll}
+ \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
+ \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
+ \isa{{\isachardoublequote}ML{\isachardoublequote}} & 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 ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would
+ cause that piece of proof to be treated as \isa{invisible} instead
+ of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden
+ depending on the document setup. In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' 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, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' would force the
+ whole sub-proof to be typeset as \isa{visible} (unless some of its
+ parts are tagged differently).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Draft presentation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('display\_drafts' | 'print\_drafts') (name +)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{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}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon Jun 02 22:50:29 2008 +0200
@@ -24,733 +24,7 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Specification commands%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Derived specifications%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
- \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
- \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- These specification mechanisms provide a slightly more abstract view
- than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see
- \secref{sec:axms-thms}). In particular, type-inference is commonly
- available, and result names need not be given.
-
- \begin{rail}
- 'axiomatization' target? fixes? ('where' specs)?
- ;
- 'definition' target? (decl 'where')? thmdecl? prop
- ;
- 'abbreviation' target? mode? (decl 'where')? prop
- ;
- ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
- ;
-
- fixes: ((name ('::' type)? mixfix? | vars) + 'and')
- ;
- specs: (thmdecl? props + 'and')
- ;
- decl: name ('::' type)? mixfix?
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants
- simultaneously and states axiomatic properties for these. The
- constants are marked as being specified once and for all, which
- prevents additional specifications being issued later on.
-
- Note that axiomatic specifications are only appropriate when
- declaring a new logical system. Normal applications should only use
- definitional mechanisms!
-
- \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
- internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
- given as \isa{eq}, which is then turned into a proven fact. The
- given proposition may deviate from internal meta-level equality
- according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
- object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not
- change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
-
- Definitions may be presented with explicit arguments on the LHS, as
- well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
- \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an
- unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
-
- \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces
- a syntactic constant which is associated with a certain term
- according to the meta-level equality \isa{eq}.
-
- Abbreviations participate in the usual type-inference process, but
- are expanded before the logic ever sees them. Pretty printing of
- terms involves higher-order rewriting with rules stemming from
- reverted abbreviations. This needs some care to avoid overlapping
- or looping syntactic replacements!
-
- The optional \isa{mode} specification restricts output to a
- particular print mode; using ``\isa{input}'' here achieves the
- effect of one-way abbreviations. The mode may also include an
- ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
- declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
- \secref{sec:syn-trans}.
-
- \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
- of the current context.
-
- \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
- syntax with an existing constant or fixed variable. This is a
- robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
- (\secref{sec:syn-trans}). Type declaration and internal syntactic
- representation of the given entity is retrieved from the context.
-
- \item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the
- present context.
-
- \end{descr}
-
- All of these specifications support local theory targets (cf.\
- \secref{sec:target}).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Generic declarations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Arbitrary operations on the background context may be wrapped-up as
- generic declaration elements. Since the underlying concept of local
- theories may be subject to later re-interpretation, there is an
- additional dependency on a morphism that tells the difference of the
- original declaration context wrt.\ the application context
- encountered later on. A fact declaration is an important special
- case: it consists of a theorem which is applied to the context by
- means of an attribute.
-
- \begin{matharray}{rcl}
- \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- \begin{rail}
- 'declaration' target? text
- ;
- 'declare' target? (thmrefs + 'and')
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration
- function \isa{d} of ML type \verb|declaration|, to the current
- local theory under construction. In later application contexts, the
- function is transformed according to the morphisms being involved in
- the interpretation hierarchy.
-
- \item [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the
- current local theory context. No theorem binding is involved here,
- unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
- \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
- of applying attributes as included in the theorem specification.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Local theory targets \label{sec:target}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A local theory target is a context managed separately within the
- enclosing theory. Contexts may introduce parameters (fixed
- variables) and assumptions (hypotheses). Definitions and theorems
- depending on the context may be added incrementally later on. Named
- contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
- (cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
- global theory context.
-
- \begin{matharray}{rcll}
- \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
- \indexdef{}{command}{end}\hypertarget{command.end}{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\
- \end{matharray}
-
- \indexouternonterm{target}
- \begin{rail}
- 'context' name 'begin'
- ;
-
- target: '(' 'in' name ')'
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
- existing locale or class context \isa{c}. Note that locale and
- class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}
- keyword as well, in order to continue the local theory immediately
- after the initial specification.
-
- \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory and
- continues the enclosing global theory. Note that a non-local
- \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory
- itself (\secref{sec:begin-thy}).
-
- \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command
- specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or
- global theory context; the current target context will be suspended
- for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
- always produce a global result independently of the current target
- context.
-
- \end{descr}
-
- The exact meaning of results produced within a local theory context
- depends on the underlying target infrastructure (locale, type class
- etc.). The general idea is as follows, considering a context named
- \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
-
- Definitions are exported by introducing a global version with
- additional arguments; a syntactic abbreviation links the long form
- with the abstract version of the target context. For example,
- \isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory
- level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
- abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
- fixed parameter \isa{x}).
-
- Theorems are exported by discharging the assumptions and
- generalizing the parameters of the context. For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary
- \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Locales \label{sec:locale}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locales are named local contexts, consisting of a list of
- declaration elements that are modeled after the Isar proof context
- commands (cf.\ \secref{sec:proof-context}).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Locale specifications%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
- \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
- \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
- \end{matharray}
-
- \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
- \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
- \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
- \begin{rail}
- 'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
- ;
- 'print\_locale' '!'? localeexpr
- ;
- localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
- ;
-
- contextexpr: nameref | '(' contextexpr ')' |
- (contextexpr (name mixfix? +)) | (contextexpr + '+')
- ;
- contextelem: fixes | constrains | assumes | defines | notes
- ;
- fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
- ;
- constrains: 'constrains' (name '::' type + 'and')
- ;
- assumes: 'assumes' (thmdecl? props + 'and')
- ;
- defines: 'defines' (thmdecl? prop proppat? + 'and')
- ;
- notes: 'notes' (thmdef? thmrefs + 'and')
- ;
- includes: 'includes' contextexpr
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] defines a
- new locale \isa{loc} as a context consisting of a certain view of
- existing locales (\isa{import}) plus some additional elements
- (\isa{body}). Both \isa{import} and \isa{body} are optional;
- the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
- locale, which may still be useful to collect declarations of facts
- later on. Type-inference on locale expressions automatically takes
- care of the most general typing that the combined context elements
- may acquire.
-
- The \isa{import} consists of a structured context expression,
- consisting of references to existing locales, renamed contexts, or
- merged contexts. Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
- parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
- position. Renaming by default deletes concrete syntax, but new
- syntax may by specified with a mixfix annotation. An exeption of
- this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
- be changed. Merging proceeds from left-to-right, suppressing any
- duplicates stemming from different paths through the import
- hierarchy.
-
- The \isa{body} consists of basic context elements, further context
- expressions may be included as well.
-
- \begin{descr}
-
- \item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local
- parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
- are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
- implicitly in this context.
-
- \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type
- constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
-
- \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}]
- introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
- proof (cf.\ \secref{sec:proof-context}).
-
- \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously
- declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
- proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
- takes an equational proposition instead of variable-term pair. The
- left-hand side of the equation may have additional arguments, e.g.\
- ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
-
- \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
- reconsiders facts within a local context. Most notably, this may
- include arbitrary declarations in any attribute specifications
- included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
-
- \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
- in a statically scoped manner. Only available in the long goal
- format of \secref{sec:goals}.
-
- In contrast, the initial \isa{import} specification of a locale
- expression maintains a dynamic relation to the locales being
- referenced (benefiting from any later fact declarations in the
- obvious manner).
-
- \end{descr}
-
- Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
- in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
- are illegal in locale definitions. In the long goal format of
- \secref{sec:goals}, term bindings may be included as expected,
- though.
-
- \medskip By default, locale specifications are ``closed up'' by
- turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
- (modulo local definitions). The predicate statement covers only the
- newly specified assumptions, omitting the content of included locale
- expressions. The full cumulative view is only provided on export,
- involving another predicate \isa{loc} that refers to the complete
- specification text.
-
- In any case, the predicate arguments are those locale parameters
- that actually occur in the respective piece of text. Also note that
- these predicates operate at the meta-level in theory, but the locale
- packages attempts to internalize statements according to the
- object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
- \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
- \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
-
- The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
- the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
- constructions. Predicates are also omitted for empty specification
- texts.
-
- \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
- specified locale expression in a flattened form. The notable
- special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
- contents of the named locale, but keep in mind that type-inference
- will normalize type variables according to the usual alphabetical
- order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
- Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
-
- \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
- of the current theory.
-
- \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
- repeatedly expand all introduction rules of locale predicates of the
- theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
- assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
- \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
- specifications entailed by the context, both from target and
- \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
- below). New goals that are entailed by the current context are
- discharged automatically.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Interpretation of locales%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locale expressions (more precisely, \emph{context expressions}) may
- be instantiated, and the instantiated facts added to the current
- context. This requires a proof of the instantiated specification
- and is called \emph{locale interpretation}. Interpretation is
- possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
-
- \begin{matharray}{rcl}
- \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\
- \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
- \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \end{matharray}
-
- \indexouternonterm{interp}
- \begin{rail}
- 'interpretation' (interp | name ('<' | subseteq) contextexpr)
- ;
- 'interpret' interp
- ;
- 'print\_interps' '!'? name
- ;
- instantiation: ('[' (inst+) ']')?
- ;
- interp: thmdecl? \\ (contextexpr instantiation |
- name instantiation 'where' (thmdecl? prop + 'and'))
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
-
- The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms
- \isa{insts} and is positional. All parameters must receive an
- instantiation term --- with the exception of defined parameters.
- These are, if omitted, derived from the defining equation and other
- instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
-
- The command generates proof obligations for the instantiated
- specifications (assumes and defines elements). Once these are
- discharged by the user, instantiated facts are added to the theory
- in a post-processing phase.
-
- Additional equations, which are unfolded in facts during
- post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
- This is useful for interpreting concepts introduced through
- definition specification elements. The equations must be proved.
- Note that if equations are present, the context expression is
- restricted to a locale name.
-
- The command is aware of interpretations already active in the
- theory. No proof obligations are generated for those, neither is
- post-processing applied to their facts. This avoids duplication of
- interpreted facts, in particular. Note that, in the case of a
- locale with import, parts of the interpretation may already be
- active. The command will only generate proof obligations and
- process facts for new parts.
-
- The context expression may be preceded by a name and/or attributes.
- These take effect in the post-processing of facts. The name is used
- to prefix fact names, for example to avoid accidental hiding of
- other facts. Attributes are applied after attributes of the
- interpreted facts.
-
- Adding facts to locales has the effect of adding interpreted facts
- to the theory for all active interpretations also. That is,
- interpretations dynamically participate in any facts added to
- locales.
-
- \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]
-
- This form of the command interprets \isa{expr} in the locale
- \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the
- localized version of the theorem command, the proof is in the
- context of \isa{name}. After the proof obligation has been
- dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
- context \isa{name} is subsequently entered. Note that, like
- import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
- Like facts of renamed context elements, facts obtained by
- interpretation may be accessed by prefixing with the parameter
- renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
-
- Unlike interpretation in theories, instantiation is confined to the
- renaming of parameters, which may be specified as part of the
- context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
-
- Only specification fragments of \isa{expr} that are not already
- part of \isa{name} (be it imported, derived or a derived fragment
- of the import) are considered by interpretation. This enables
- circular interpretations.
-
- If interpretations of \isa{name} exist in the current theory, the
- command adds interpretations for \isa{expr} as well, with the same
- prefix and attributes, although only for fragments of \isa{expr}
- that are not interpreted in the theory already.
-
- \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
- interprets \isa{expr} in the proof context and is otherwise
- similar to interpretation in theories.
-
- \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
- interpretations of a particular locale \isa{loc} that are active
- in the current context, either theory or proof context. The
- exclamation point argument triggers printing of \emph{witness}
- theorems justifying interpretations. These are normally omitted
- from the output.
-
- \end{descr}
-
- \begin{warn}
- Since attributes are applied to interpreted theorems,
- interpretation may modify the context of common proof tools, e.g.\
- the Simplifier or Classical Reasoner. Since the behavior of such
- automated reasoning tools is \emph{not} stable under
- interpretation morphisms, manual declarations might have to be
- issued.
- \end{warn}
-
- \begin{warn}
- An interpretation in a theory may subsume previous
- interpretations. This happens if the same specification fragment
- is interpreted twice and the instantiation of the second
- interpretation is more general than the interpretation of the
- first. A warning is issued, since it is likely that these could
- have been generalized in the first place. The locale package does
- not attempt to remove subsumed interpretations.
- \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Classes \label{sec:class}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A class is a particular locale with \emph{exactly one} type variable
- \isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
- is established which is interpreted logically as axiomatic type
- class \cite{Wenzel:1997:TPHOL} whose logical content are the
- assumptions of the locale. Thus, classes provide the full
- generality of locales combined with the commodity of type classes
- (notably type-inference). See \cite{isabelle-classes} for a short
- tutorial.
-
- \begin{matharray}{rcl}
- \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
- \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
- \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
- \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
- \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
- \end{matharray}
-
- \begin{rail}
- 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
- 'begin'?
- ;
- 'instantiation' (nameref + 'and') '::' arity 'begin'
- ;
- 'instance'
- ;
- 'subclass' target? nameref
- ;
- 'print\_classes'
- ;
-
- superclassexpr: nameref | (nameref '+' superclassexpr)
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines
- a new class \isa{c}, inheriting from \isa{superclasses}. This
- introduces a locale \isa{c} with import of all locales \isa{superclasses}.
-
- Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
- theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter
- \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
-
- Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
- mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
- corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
- corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
- --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
- class membership proofs.
-
- \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\
- \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the
- particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
- in the target body poses a goal stating these type arities. The
- target is concluded by an \indexref{}{command}{end}\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} command.
-
- Note that a list of simultaneous type constructors may be given;
- this corresponds nicely to mutual recursive type definitions, e.g.\
- in Isabelle/HOL.
-
- \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets
- up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
- the type classes involved. After finishing the proof, the
- background theory will be augmented by the proven type arities.
-
- \item [\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c}] in a class context for class
- \isa{d} sets up a goal stating that class \isa{c} is logically
- contained in class \isa{d}. After finishing the proof, class
- \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
-
- \item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
- theory.
-
- \item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
- introduction rules of this theory. Note that this method usually
- needs not be named explicitly, as it is already included in the
- default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
- instantiation of trivial (syntactic) classes may be performed by a
- single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The class target%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-%FIXME check
-
- A named context may refer to a locale (cf.\ \secref{sec:target}).
- If this locale is also a class \isa{c}, apart from the common
- locale target behaviour the following happens.
-
- \begin{itemize}
-
- \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
- local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
- are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
- referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
-
- \item Local theorem bindings are lifted as are assumptions.
-
- \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
- global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
- resolves ambiguities. In rare cases, manual type annotations are
- needed.
-
- \end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Axiomatic type classes \label{sec:axclass}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
- \end{matharray}
-
- Axiomatic type classes are Isabelle/Pure's primitive
- \emph{definitional} interface to type classes. For practical
- applications, you should consider using classes
- (cf.~\secref{sec:classes}) which provide high level interface.
-
- \begin{rail}
- 'axclass' classdecl (axmdecl prop +)
- ;
- 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of
- existing classes, with additional axioms holding. Class axioms may
- not contain more than one type variable. The class axioms (with
- implicit sort constraints added) are bound to the given names.
- Furthermore a class introduction rule is generated (being bound as
- \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
-
- The ``class axioms'' are stored as theorems according to the given
- name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
- the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
-
- \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
- \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}]
- setup a goal stating a class relation or type arity. The proof
- would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
- the characteristic theorems of the type classes involved. After
- finishing the proof, the theory will be augmented by a type
- signature declaration corresponding to the resulting theorem.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Arbitrary overloading%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle/Pure's definitional schemes support certain forms of
- overloading (see \secref{sec:consts}). At most occassions
- overloading will be used in a Haskell-like fashion together with
- type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
- \secref{sec:class}). Sometimes low-level overloading is desirable.
- The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
- end-users.
-
- \begin{matharray}{rcl}
- \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
- \end{matharray}
-
- \begin{rail}
- 'overloading' \\
- ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}]
- opens a theory target (cf.\ \secref{sec:target}) which allows to
- specify constants with overloaded definitions. These are identified
- by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type
- instances. The definitions themselves are established using common
- specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as
- reference to the corresponding constants. The target is concluded
- by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}.
-
- A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
- the corresponding definition, which is occasionally useful for
- exotic overloading. It is at the discretion of the user to avoid
- malformed theory specifications!
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Configuration options%
+\isamarkupsection{Configuration options%
}
\isamarkuptrue%
%
@@ -790,7 +64,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof tools%
+\isamarkupsection{Basic proof tools%
}
\isamarkuptrue%
%
@@ -1031,11 +305,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{The Simplifier \label{sec:simplifier}%
+\isamarkupsection{The Simplifier \label{sec:simplifier}%
}
\isamarkuptrue%
%
-\isamarkupsubsubsection{Simplification methods%
+\isamarkupsubsection{Simplification methods%
}
\isamarkuptrue%
%
@@ -1110,7 +384,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Declaring rules%
+\isamarkupsubsection{Declaring rules%
}
\isamarkuptrue%
%
@@ -1143,7 +417,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Simplification procedures%
+\isamarkupsubsection{Simplification procedures%
}
\isamarkuptrue%
%
@@ -1189,7 +463,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Forward simplification%
+\isamarkupsubsection{Forward simplification%
}
\isamarkuptrue%
%
@@ -1224,7 +498,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Low-level equational reasoning%
+\isamarkupsubsection{Low-level equational reasoning%
}
\isamarkuptrue%
%
@@ -1290,11 +564,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{The Classical Reasoner \label{sec:classical}%
+\isamarkupsection{The Classical Reasoner \label{sec:classical}%
}
\isamarkuptrue%
%
-\isamarkupsubsubsection{Basic methods%
+\isamarkupsubsection{Basic methods%
}
\isamarkuptrue%
%
@@ -1339,7 +613,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Automated methods%
+\isamarkupsubsection{Automated methods%
}
\isamarkuptrue%
%
@@ -1384,7 +658,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Combined automated methods \label{sec:clasimp}%
+\isamarkupsubsection{Combined automated methods \label{sec:clasimp}%
}
\isamarkuptrue%
%
@@ -1430,7 +704,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Declaring rules%
+\isamarkupsubsection{Declaring rules%
}
\isamarkuptrue%
%
@@ -1486,7 +760,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Classical operations%
+\isamarkupsubsection{Classical operations%
}
\isamarkuptrue%
%
@@ -1504,355 +778,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Proof by cases and induction \label{sec:cases-induct}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Rule contexts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
- \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
- \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\
- \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\
- \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isaratt \\
- \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isaratt \\
- \end{matharray}
-
- The puristic way to build up Isar proof contexts is by explicit
- language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
- \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}). This is adequate
- for plain natural deduction, but easily becomes unwieldy in concrete
- verification tasks, which typically involve big induction rules with
- several cases.
-
- The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a
- local context symbolically: certain proof methods provide an
- environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. Term bindings may be covered as well, notably
- \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion.
-
- By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of
- a case value is marked as hidden, i.e.\ there is no way to refer to
- such parameters in the subsequent proof text. After all, original
- rule parameters stem from somewhere outside of the current proof
- text. By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to
- chose local names that fit nicely into the current context.
-
- \medskip It is important to note that proper use of \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} does not provide means to peek at the current goal state,
- which is not directly observable in Isar! Nonetheless, goal
- refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}}
- for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state.
- Using this extra feature requires great care, because some bits of
- the internal tactical machinery intrude the proof text. In
- particular, parameter names stemming from the left-over of automated
- reasoning tools are usually quite unpredictable.
-
- Under normal circumstances, the text of cases emerge from standard
- elimination or induction rules, which in turn are derived from
- previous theory specifications in a canonical way (say from
- \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).
-
- \medskip Proper cases are only available if both the proof method
- and the rules involved support this. By using appropriate
- attributes, case names, conclusions, and parameters may be also
- declared by hand. Thus variant versions of rules that have been
- derived manually become ready to use in advanced case analysis
- later.
-
- \begin{rail}
- 'case' (caseref | '(' caseref ((name | underscore) +) ')')
- ;
- caseref: nameref attributes?
- ;
-
- 'case\_names' (name +)
- ;
- 'case\_conclusion' name (name *)
- ;
- 'params' ((name *) + 'and')
- ;
- 'consumes' nat?
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}]
- invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate
- proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).
- The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.
-
- \item [\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the
- current state, using Isar proof language notation.
-
- \item [\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}]
- declares names for the local contexts of premises of a theorem;
- \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the
- list of premises.
-
- \item [\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise
- \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the
- prefix of arguments of a logical formula built by nesting a binary
- connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
-
- Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} already provide a default name for the conclusion as a
- whole. The need to name subformulas only arises with cases that
- split into several sub-cases, as in common co-induction rules.
-
- \item [\hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of
- premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some theorem. An empty list of names
- may be given to skip positions, leaving the present parameters
- unchanged.
-
- Note that the default usage of case rules does \emph{not} directly
- expose parameters to the proof context.
-
- \item [\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n}] declares the number of
- ``major premises'' of a rule, i.e.\ the number of facts to be
- consumed when it is applied by an appropriate proof method. The
- default value of \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is
- appropriate for the usual kind of cases and induction rules for
- inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
- \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if
- \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified.
-
- Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only
- rarely needed; this is already taken care of automatically by the
- higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and
- \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Proof methods%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isarmeth \\
- \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isarmeth \\
- \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isarmeth \\
- \end{matharray}
-
- The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
- methods provide a uniform interface to common proof techniques over
- datatypes, inductive predicates (or sets), recursive functions etc.
- The corresponding rules may be specified and instantiated in a
- casual manner. Furthermore, these methods provide named local
- contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command
- within the subsequent proof text. This accommodates compact proof
- texts even when reasoning about large specifications.
-
- The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional
- infrastructure in order to be applicable to structure statements
- (either using explicit meta-level connectives, or including facts
- and parameters separately). This avoids cumbersome encoding of
- ``strengthened'' inductive statements within the object-logic.
-
- \begin{rail}
- 'cases' (insts * 'and') rule?
- ;
- 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
- ;
- 'coinduct' insts taking rule?
- ;
-
- rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
- ;
- definst: name ('==' | equiv) term | inst
- ;
- definsts: ( definst *)
- ;
- arbitrary: 'arbitrary' ':' ((term *) 'and' +)
- ;
- taking: 'taking' ':' insts
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to
- the subjects \isa{insts}. Symbolic case names are bound according
- to the rule's local contexts.
-
- The rule is determined as follows, according to the facts and
- arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:
-
- \medskip
- \begin{tabular}{llll}
- facts & & arguments & rule \\\hline
- & \hyperlink{method.cases}{\mbox{\isa{cases}}} & & classical case split \\
- & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\
- \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\
- \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
- \end{tabular}
- \medskip
-
- Several instantiations may be given, referring to the \emph{suffix}
- of premises of the case rule; within each premise, the \emph{prefix}
- of variables is instantiated. In most situations, only a single
- term needs to be specified; this refers to the first variable of the
- last premise (it is usually the same for all cases).
-
- \item [\hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the
- \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
- determined as follows:
-
- \medskip
- \begin{tabular}{llll}
- facts & & arguments & rule \\\hline
- & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\
- \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\
- \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
- \end{tabular}
- \medskip
-
- Several instantiations may be given, each referring to some part of
- a mutual inductive definition or datatype --- only related partial
- induction rules may be used together, though. Any of the lists of
- terms \isa{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} refers to the \emph{suffix} of variables
- present in the induction rule. This enables the writer to specify
- only induction variables, or both predicates and variables, for
- example.
-
- Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
- introduce local definitions, which are inserted into the claim and
- discharged after applying the induction rule. Equalities reappear
- in the inductive cases, but have been transformed according to the
- induction principle being involved here. In order to achieve
- practically useful induction hypotheses, some variables occurring in
- \isa{t} need to be fixed (see below).
-
- The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
- specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus
- induction hypotheses may become sufficiently general to get the
- proof through. Together with definitional instantiations, one may
- effectively perform induction over expressions of a certain
- structure.
-
- The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
- specification provides additional instantiations of a prefix of
- pending variables in the rule. Such schematic induction rules
- rarely occur in practice, though.
-
- \item [\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the
- \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are
- determined as follows:
-
- \medskip
- \begin{tabular}{llll}
- goal & & arguments & rule \\\hline
- & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\
- \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\
- \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
- \end{tabular}
-
- Coinduction is the dual of induction. Induction essentially
- eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}},
- while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}. The cases of a
- coinduct rule are typically named after the predicates or sets being
- covered, while the conclusions consist of several alternatives being
- named after the individual destructor patterns.
-
- The given instantiation refers to the \emph{suffix} of variables
- occurring in the rule's major premise, or conclusion if unavailable.
- An additional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
- specification may be required in order to specify the bisimulation
- to be used in the coinduction step.
-
- \end{descr}
-
- Above methods produce named local contexts, as determined by the
- instantiated rule as given in the text. Beyond that, the \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} methods guess further instantiations
- from the goal specification itself. Any persisting unresolved
- schematic variables of the resulting rule will render the the
- corresponding case invalid. The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for
- the conclusion will be provided with each case, provided that term
- is fully specified.
-
- The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
- in the current proof state.
-
- \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
- and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after
- instantiation, while conforming due to the usual way of monotonic
- natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}
- reappears unchanged after the case split.
-
- The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this
- respect: the meta-level structure is passed through the
- ``recursive'' course involved in the induction. Thus the original
- statement is basically replaced by separate copies, corresponding to
- the induction hypotheses and conclusion; the original goal context
- is no longer available. Thus local assumptions, fixed parameters
- and definitions effectively participate in the inductive rephrasing
- of the original statement.
-
- In induction proofs, local assumptions introduced by cases are split
- into two different kinds: \isa{hyps} stemming from the rule and
- \isa{prems} from the goal statement. This is reflected in the
- extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
- as well as fact \isa{c} to hold the all-inclusive list.
-
- \medskip Facts presented to either method are consumed according to
- the number of ``major premises'' of the rule involved, which is
- usually 0 for plain cases and induction rules of datatypes etc.\ and
- 1 for rules of inductive predicates or sets and the like. The
- remaining facts are inserted into the goal verbatim before the
- actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
- applied.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Declaring rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isaratt \\
- \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isaratt \\
- \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isaratt \\
- \end{matharray}
-
- \begin{rail}
- 'cases' spec
- ;
- 'induct' spec
- ;
- 'coinduct' spec
- ;
-
- spec: ('type' | 'pred' | 'set') ':' nameref
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct
- rules for predicates (or sets) and types of the current context.
-
- \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}] (as attributes) augment the corresponding context of
- rules for reasoning about (co)inductive predicates (or sets) and
- types, using the corresponding methods of the same name. Certain
- definitional packages of object-logics usually declare emerging
- cases and induction rules as expected, so users rarely need to
- intervene.
-
- Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
- cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
- declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{General logic setup \label{sec:object-logic}%
}
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 02 22:50:29 2008 +0200
@@ -1154,7 +1154,6 @@
%
\endisadelimtheory
\isanewline
-\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/Thy/document/Introduction.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex Mon Jun 02 22:50:29 2008 +0200
@@ -73,10 +73,22 @@
\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 ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -108,7 +120,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Proof General%
+\isamarkupsubsection{Emacs Proof General%
}
\isamarkuptrue%
%
@@ -198,7 +210,7 @@
hand, the plain ASCII sources easily become somewhat unintelligible.
For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| 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.%
@@ -243,58 +255,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Document preparation \label{sec:document-prep}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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 \verb|mkdir| and \verb|make|
- tools. First invoke
-\begin{ttbox}
- isatool mkdir Foo
-\end{ttbox}
- to initialize a separate directory for session \verb|Foo| ---
- it is safe to experiment, since \verb|isatool mkdir| never
- overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
- holds ML commands to load all theories required for this session;
- furthermore \verb|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 \verb|IsaMakefile|
- (with crude source dependencies by default). This file is located
- one level up from the \verb|Foo| directory location. Now
- invoke
-\begin{ttbox}
- isatool make Foo
-\end{ttbox}
- to run the \verb|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
- \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
- verbose mode.
-
- \medskip You may also consider to tune the \verb|usedir|
- options in \verb|IsaMakefile|, for example to change the output
- format from \verb|pdf| to \verb|dvi|, or activate the
- \verb|-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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
}
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Jun 02 22:50:29 2008 +0200
@@ -20,7 +20,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Syntax primitives%
+\isamarkupchapter{Outer syntax%
}
\isamarkuptrue%
%
@@ -496,276 +496,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Antiquotations \label{sec:antiq}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}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 ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
- 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,
- \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ sym\ {\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}{\isacharbraceright}{\isachardoublequote}} 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 \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| or verbatim
- text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
-
- \begin{descr}
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}}] prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
- guaranteed to refer to a valid ancestor theory in the current
- context.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
- \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
- may be included as well (see also \secref{sec:syn-att}); the
- \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
- be particularly useful to suppress printing of schematic variables.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant
- \isa{{\isachardoublequote}c{\isachardoublequote}}.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints a constant
- abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in
- the current context.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}}] prints the type of a well-typed term
- \isa{{\isachardoublequote}t{\isachardoublequote}}.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}}] prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}}] prints theorem \isa{a},
- previously applying a style \isa{s} to it (see below).
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{t} after applying a style \isa{s} to it (see below).
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}}] prints uninterpreted source text \isa{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 [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}] 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 [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}}] is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
- does not print the main goal.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints the (compact)
- proof terms corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. 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 [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] is like \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}, but displays the full proof terms,
- i.e.\ also displays information omitted in the compact proof term,
- which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
-
- \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}{\isachardoublequote}}] check text \isa{s} as ML value, type, and
- structure, respectively. The source is displayed verbatim.
-
- \end{descr}
-
- \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
-
- \begin{descr}
-
- \item [\isa{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 [\isa{rhs}] is like \isa{lhs}, but extracts the second
- argument.
-
- \item [\isa{{\isachardoublequote}concl{\isachardoublequote}}] extracts the conclusion \isa{C} from a rule
- in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
-
- \item [\isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}}] extract premise
- number \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in
- Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
-
- \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[\isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}]
- control printing of explicit type and sort constraints.
-
- \item[\isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}}] controls printing of implicit
- structures.
-
- \item[\isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
- constants etc.\ to be printed in their fully qualified internal
- form.
-
- \item[\isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] 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[\isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] determines whether the printed
- version of qualified names should be made sufficiently long to avoid
- overlap with names declared further back. Set to \isa{false} for
- more concise output.
-
- \item[\isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}}] prints terms in \isa{{\isasymeta}}-contracted form.
-
- \item[\isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}}] 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[\isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}}] controls line breaks in non-display
- material.
-
- \item[\isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the output should be
- enclosed in double quotes.
-
- \item[\isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}}] adds \isa{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 \isa{latex} and \isa{xsymbols}.
-
- \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the
- margin or indentation for pretty printing of display material.
-
- \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the
- antiquotation arguments, rather than the actual value. Note that
- this does not affect well-formedness checks of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. (only the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation admits arbitrary output).
-
- \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of
- goals to be printed.
-
- \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale
- context used for evaluating and printing the subsequent argument.
-
- \end{descr}
-
- For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
- ``\isa{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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Tagged commands \label{sec:tags}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Each Isabelle/Isar command may be decorated by presentation tags:
-
- \indexouternonterm{tags}
- \begin{rail}
- tags: ( tag * )
- ;
- tag: '\%' (ident | string)
- \end{rail}
-
- The tags \isa{{\isachardoublequote}theory{\isachardoublequote}}, \isa{{\isachardoublequote}proof{\isachardoublequote}}, \isa{{\isachardoublequote}ML{\isachardoublequote}} are already
- pre-declared for certain classes of commands:
-
- \medskip
-
- \begin{tabular}{ll}
- \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
- \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
- \isa{{\isachardoublequote}ML{\isachardoublequote}} & 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 ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would
- cause that piece of proof to be treated as \isa{invisible} instead
- of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden
- depending on the document setup. In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' 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, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' would force the
- whole sub-proof to be typeset as \isa{visible} (unless some of its
- parts are tagged differently).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 02 22:50:29 2008 +0200
@@ -1018,6 +1018,355 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Proof by cases and induction \label{sec:cases-induct}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Rule contexts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
+ \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\
+ \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\
+ \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isaratt \\
+ \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isaratt \\
+ \end{matharray}
+
+ The puristic way to build up Isar proof contexts is by explicit
+ language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
+ \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}). This is adequate
+ for plain natural deduction, but easily becomes unwieldy in concrete
+ verification tasks, which typically involve big induction rules with
+ several cases.
+
+ The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a
+ local context symbolically: certain proof methods provide an
+ environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''. Term bindings may be covered as well, notably
+ \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion.
+
+ By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of
+ a case value is marked as hidden, i.e.\ there is no way to refer to
+ such parameters in the subsequent proof text. After all, original
+ rule parameters stem from somewhere outside of the current proof
+ text. By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to
+ chose local names that fit nicely into the current context.
+
+ \medskip It is important to note that proper use of \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} does not provide means to peek at the current goal state,
+ which is not directly observable in Isar! Nonetheless, goal
+ refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}}
+ for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state.
+ Using this extra feature requires great care, because some bits of
+ the internal tactical machinery intrude the proof text. In
+ particular, parameter names stemming from the left-over of automated
+ reasoning tools are usually quite unpredictable.
+
+ Under normal circumstances, the text of cases emerge from standard
+ elimination or induction rules, which in turn are derived from
+ previous theory specifications in a canonical way (say from
+ \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).
+
+ \medskip Proper cases are only available if both the proof method
+ and the rules involved support this. By using appropriate
+ attributes, case names, conclusions, and parameters may be also
+ declared by hand. Thus variant versions of rules that have been
+ derived manually become ready to use in advanced case analysis
+ later.
+
+ \begin{rail}
+ 'case' (caseref | '(' caseref ((name | underscore) +) ')')
+ ;
+ caseref: nameref attributes?
+ ;
+
+ 'case\_names' (name +)
+ ;
+ 'case\_conclusion' name (name *)
+ ;
+ 'params' ((name *) + 'and')
+ ;
+ 'consumes' nat?
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}]
+ invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate
+ proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).
+ The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.
+
+ \item [\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the
+ current state, using Isar proof language notation.
+
+ \item [\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}]
+ declares names for the local contexts of premises of a theorem;
+ \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the
+ list of premises.
+
+ \item [\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise
+ \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the
+ prefix of arguments of a logical formula built by nesting a binary
+ connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
+
+ Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} already provide a default name for the conclusion as a
+ whole. The need to name subformulas only arises with cases that
+ split into several sub-cases, as in common co-induction rules.
+
+ \item [\hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of
+ premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some theorem. An empty list of names
+ may be given to skip positions, leaving the present parameters
+ unchanged.
+
+ Note that the default usage of case rules does \emph{not} directly
+ expose parameters to the proof context.
+
+ \item [\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n}] declares the number of
+ ``major premises'' of a rule, i.e.\ the number of facts to be
+ consumed when it is applied by an appropriate proof method. The
+ default value of \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is
+ appropriate for the usual kind of cases and induction rules for
+ inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
+ \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if
+ \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified.
+
+ Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only
+ rarely needed; this is already taken care of automatically by the
+ higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and
+ \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Proof methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isarmeth \\
+ \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isarmeth \\
+ \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isarmeth \\
+ \end{matharray}
+
+ The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
+ methods provide a uniform interface to common proof techniques over
+ datatypes, inductive predicates (or sets), recursive functions etc.
+ The corresponding rules may be specified and instantiated in a
+ casual manner. Furthermore, these methods provide named local
+ contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command
+ within the subsequent proof text. This accommodates compact proof
+ texts even when reasoning about large specifications.
+
+ The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional
+ infrastructure in order to be applicable to structure statements
+ (either using explicit meta-level connectives, or including facts
+ and parameters separately). This avoids cumbersome encoding of
+ ``strengthened'' inductive statements within the object-logic.
+
+ \begin{rail}
+ 'cases' (insts * 'and') rule?
+ ;
+ 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
+ ;
+ 'coinduct' insts taking rule?
+ ;
+
+ rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
+ ;
+ definst: name ('==' | equiv) term | inst
+ ;
+ definsts: ( definst *)
+ ;
+ arbitrary: 'arbitrary' ':' ((term *) 'and' +)
+ ;
+ taking: 'taking' ':' insts
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to
+ the subjects \isa{insts}. Symbolic case names are bound according
+ to the rule's local contexts.
+
+ The rule is determined as follows, according to the facts and
+ arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:
+
+ \medskip
+ \begin{tabular}{llll}
+ facts & & arguments & rule \\\hline
+ & \hyperlink{method.cases}{\mbox{\isa{cases}}} & & classical case split \\
+ & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\
+ \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\
+ \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
+ \end{tabular}
+ \medskip
+
+ Several instantiations may be given, referring to the \emph{suffix}
+ of premises of the case rule; within each premise, the \emph{prefix}
+ of variables is instantiated. In most situations, only a single
+ term needs to be specified; this refers to the first variable of the
+ last premise (it is usually the same for all cases).
+
+ \item [\hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the
+ \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
+ determined as follows:
+
+ \medskip
+ \begin{tabular}{llll}
+ facts & & arguments & rule \\\hline
+ & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}} & datatype induction (type of \isa{x}) \\
+ \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set induction (of \isa{A}) \\
+ \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
+ \end{tabular}
+ \medskip
+
+ Several instantiations may be given, each referring to some part of
+ a mutual inductive definition or datatype --- only related partial
+ induction rules may be used together, though. Any of the lists of
+ terms \isa{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} refers to the \emph{suffix} of variables
+ present in the induction rule. This enables the writer to specify
+ only induction variables, or both predicates and variables, for
+ example.
+
+ Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
+ introduce local definitions, which are inserted into the claim and
+ discharged after applying the induction rule. Equalities reappear
+ in the inductive cases, but have been transformed according to the
+ induction principle being involved here. In order to achieve
+ practically useful induction hypotheses, some variables occurring in
+ \isa{t} need to be fixed (see below).
+
+ The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
+ specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus
+ induction hypotheses may become sufficiently general to get the
+ proof through. Together with definitional instantiations, one may
+ effectively perform induction over expressions of a certain
+ structure.
+
+ The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
+ specification provides additional instantiations of a prefix of
+ pending variables in the rule. Such schematic induction rules
+ rarely occur in practice, though.
+
+ \item [\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the
+ \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are
+ determined as follows:
+
+ \medskip
+ \begin{tabular}{llll}
+ goal & & arguments & rule \\\hline
+ & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\
+ \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\
+ \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
+ \end{tabular}
+
+ Coinduction is the dual of induction. Induction essentially
+ eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}},
+ while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}. The cases of a
+ coinduct rule are typically named after the predicates or sets being
+ covered, while the conclusions consist of several alternatives being
+ named after the individual destructor patterns.
+
+ The given instantiation refers to the \emph{suffix} of variables
+ occurring in the rule's major premise, or conclusion if unavailable.
+ An additional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
+ specification may be required in order to specify the bisimulation
+ to be used in the coinduction step.
+
+ \end{descr}
+
+ Above methods produce named local contexts, as determined by the
+ instantiated rule as given in the text. Beyond that, the \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} methods guess further instantiations
+ from the goal specification itself. Any persisting unresolved
+ schematic variables of the resulting rule will render the the
+ corresponding case invalid. The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for
+ the conclusion will be provided with each case, provided that term
+ is fully specified.
+
+ The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
+ in the current proof state.
+
+ \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
+ and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after
+ instantiation, while conforming due to the usual way of monotonic
+ natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}
+ reappears unchanged after the case split.
+
+ The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this
+ respect: the meta-level structure is passed through the
+ ``recursive'' course involved in the induction. Thus the original
+ statement is basically replaced by separate copies, corresponding to
+ the induction hypotheses and conclusion; the original goal context
+ is no longer available. Thus local assumptions, fixed parameters
+ and definitions effectively participate in the inductive rephrasing
+ of the original statement.
+
+ In induction proofs, local assumptions introduced by cases are split
+ into two different kinds: \isa{hyps} stemming from the rule and
+ \isa{prems} from the goal statement. This is reflected in the
+ extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
+ as well as fact \isa{c} to hold the all-inclusive list.
+
+ \medskip Facts presented to either method are consumed according to
+ the number of ``major premises'' of the rule involved, which is
+ usually 0 for plain cases and induction rules of datatypes etc.\ and
+ 1 for rules of inductive predicates or sets and the like. The
+ remaining facts are inserted into the goal verbatim before the
+ actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
+ applied.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Declaring rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isaratt \\
+ \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isaratt \\
+ \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isaratt \\
+ \end{matharray}
+
+ \begin{rail}
+ 'cases' spec
+ ;
+ 'induct' spec
+ ;
+ 'coinduct' spec
+ ;
+
+ spec: ('type' | 'pred' | 'set') ':' nameref
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct
+ rules for predicates (or sets) and types of the current context.
+
+ \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}] (as attributes) augment the corresponding context of
+ rules for reasoning about (co)inductive predicates (or sets) and
+ types, using the corresponding methods of the same name. Certain
+ definitional packages of object-logics usually declare emerging
+ cases and induction rules as expected, so users rarely need to
+ intervene.
+
+ Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
+ cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
+ declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Jun 02 22:50:29 2008 +0200
@@ -32,21 +32,23 @@
\begin{matharray}{rcl}
\indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\
\indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\
- \indexdef{}{command}{end}\hypertarget{command.end}{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\
+ \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{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 \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}.
The first ``real'' command of any theory has to be \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which starts a new theory based on the merge of existing
ones. Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be
an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{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 \hyperlink{command.end}{\mbox{\isa{\isacommand{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
+ \hyperlink{command.global.end}{\mbox{\isa{\isacommand{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
@@ -62,8 +64,7 @@
\item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
markup just preceding the formal beginning of a theory. In actual
document preparation the corresponding {\LaTeX} macro \verb|\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 [\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the
merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
@@ -82,13 +83,1255 @@
text (typically via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} in the body text,
see \secref{sec:ML}).
- \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory definition or
- context switch.
+ \item [\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory
+ definition.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Local theory targets \label{sec:target}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A local theory target is a context managed separately within the
+ enclosing theory. Contexts may introduce parameters (fixed
+ variables) and assumptions (hypotheses). Definitions and theorems
+ depending on the context may be added incrementally later on. Named
+ contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
+ (cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
+ global theory context.
+
+ \begin{matharray}{rcll}
+ \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+ \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\
+ \end{matharray}
+
+ \indexouternonterm{target}
+ \begin{rail}
+ 'context' name 'begin'
+ ;
+
+ target: '(' 'in' name ')'
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
+ existing locale or class context \isa{c}. Note that locale and
+ class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}
+ keyword as well, in order to continue the local theory immediately
+ after the initial specification.
+
+ \item [\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory
+ and continues the enclosing global theory. Note that a global
+ \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
+ theory itself (\secref{sec:begin-thy}).
+
+ \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command
+ specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or
+ global theory context; the current target context will be suspended
+ for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
+ always produce a global result independently of the current target
+ context.
+
+ \end{descr}
+
+ The exact meaning of results produced within a local theory context
+ depends on the underlying target infrastructure (locale, type class
+ etc.). The general idea is as follows, considering a context named
+ \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
+
+ Definitions are exported by introducing a global version with
+ additional arguments; a syntactic abbreviation links the long form
+ with the abstract version of the target context. For example,
+ \isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory
+ level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
+ abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
+ fixed parameter \isa{x}).
+
+ Theorems are exported by discharging the assumptions and
+ generalizing the parameters of the context. For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary
+ \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Basic specification elements%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
+ \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
+ \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ These specification mechanisms provide a slightly more abstract view
+ than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see
+ \secref{sec:axms-thms}). In particular, type-inference is commonly
+ available, and result names need not be given.
+
+ \begin{rail}
+ 'axiomatization' target? fixes? ('where' specs)?
+ ;
+ 'definition' target? (decl 'where')? thmdecl? prop
+ ;
+ 'abbreviation' target? mode? (decl 'where')? prop
+ ;
+ ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
+ ;
+
+ fixes: ((name ('::' type)? mixfix? | vars) + 'and')
+ ;
+ specs: (thmdecl? props + 'and')
+ ;
+ decl: name ('::' type)? mixfix?
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants
+ simultaneously and states axiomatic properties for these. The
+ constants are marked as being specified once and for all, which
+ prevents additional specifications being issued later on.
+
+ Note that axiomatic specifications are only appropriate when
+ declaring a new logical system. Normal applications should only use
+ definitional mechanisms!
+
+ \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
+ internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
+ given as \isa{eq}, which is then turned into a proven fact. The
+ given proposition may deviate from internal meta-level equality
+ according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
+ object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not
+ change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
+
+ Definitions may be presented with explicit arguments on the LHS, as
+ well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
+ \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an
+ unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
+
+ \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces
+ a syntactic constant which is associated with a certain term
+ according to the meta-level equality \isa{eq}.
+
+ Abbreviations participate in the usual type-inference process, but
+ are expanded before the logic ever sees them. Pretty printing of
+ terms involves higher-order rewriting with rules stemming from
+ reverted abbreviations. This needs some care to avoid overlapping
+ or looping syntactic replacements!
+
+ The optional \isa{mode} specification restricts output to a
+ particular print mode; using ``\isa{input}'' here achieves the
+ effect of one-way abbreviations. The mode may also include an
+ ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
+ declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
+ \secref{sec:syn-trans}.
+
+ \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
+ of the current context.
+
+ \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
+ syntax with an existing constant or fixed variable. This is a
+ robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
+ (\secref{sec:syn-trans}). Type declaration and internal syntactic
+ representation of the given entity is retrieved from the context.
+
+ \item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the
+ present context.
+
+ \end{descr}
+
+ All of these specifications support local theory targets (cf.\
+ \secref{sec:target}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Generic declarations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Arbitrary operations on the background context may be wrapped-up as
+ generic declaration elements. Since the underlying concept of local
+ theories may be subject to later re-interpretation, there is an
+ additional dependency on a morphism that tells the difference of the
+ original declaration context wrt.\ the application context
+ encountered later on. A fact declaration is an important special
+ case: it consists of a theorem which is applied to the context by
+ means of an attribute.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'declaration' target? text
+ ;
+ 'declare' target? (thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration
+ function \isa{d} of ML type \verb|declaration|, to the current
+ local theory under construction. In later application contexts, the
+ function is transformed according to the morphisms being involved in
+ the interpretation hierarchy.
+
+ \item [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the
+ current local theory context. No theorem binding is involved here,
+ unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
+ \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
+ of applying attributes as included in the theorem specification.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Locales \label{sec:locale}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locales are named local contexts, consisting of a list of
+ declaration elements that are modeled after the Isar proof context
+ commands (cf.\ \secref{sec:proof-context}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Locale specifications%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+ \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
+ \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
+ \end{matharray}
+
+ \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
+ \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
+ \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
+ \begin{rail}
+ 'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
+ ;
+ 'print\_locale' '!'? localeexpr
+ ;
+ localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
+ ;
+
+ contextexpr: nameref | '(' contextexpr ')' |
+ (contextexpr (name mixfix? +)) | (contextexpr + '+')
+ ;
+ contextelem: fixes | constrains | assumes | defines | notes
+ ;
+ fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
+ ;
+ constrains: 'constrains' (name '::' type + 'and')
+ ;
+ assumes: 'assumes' (thmdecl? props + 'and')
+ ;
+ defines: 'defines' (thmdecl? prop proppat? + 'and')
+ ;
+ notes: 'notes' (thmdef? thmrefs + 'and')
+ ;
+ includes: 'includes' contextexpr
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] defines a
+ new locale \isa{loc} as a context consisting of a certain view of
+ existing locales (\isa{import}) plus some additional elements
+ (\isa{body}). Both \isa{import} and \isa{body} are optional;
+ the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
+ locale, which may still be useful to collect declarations of facts
+ later on. Type-inference on locale expressions automatically takes
+ care of the most general typing that the combined context elements
+ may acquire.
+
+ The \isa{import} consists of a structured context expression,
+ consisting of references to existing locales, renamed contexts, or
+ merged contexts. Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
+ parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
+ position. Renaming by default deletes concrete syntax, but new
+ syntax may by specified with a mixfix annotation. An exeption of
+ this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
+ be changed. Merging proceeds from left-to-right, suppressing any
+ duplicates stemming from different paths through the import
+ hierarchy.
+
+ The \isa{body} consists of basic context elements, further context
+ expressions may be included as well.
+
+ \begin{descr}
+
+ \item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local
+ parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
+ are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
+ implicitly in this context.
+
+ \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type
+ constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
+
+ \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}]
+ introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
+ proof (cf.\ \secref{sec:proof-context}).
+
+ \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously
+ declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
+ proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
+ takes an equational proposition instead of variable-term pair. The
+ left-hand side of the equation may have additional arguments, e.g.\
+ ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
+
+ \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
+ reconsiders facts within a local context. Most notably, this may
+ include arbitrary declarations in any attribute specifications
+ included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
+
+ \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
+ in a statically scoped manner. Only available in the long goal
+ format of \secref{sec:goals}.
+
+ In contrast, the initial \isa{import} specification of a locale
+ expression maintains a dynamic relation to the locales being
+ referenced (benefiting from any later fact declarations in the
+ obvious manner).
+
+ \end{descr}
+
+ Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
+ in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
+ are illegal in locale definitions. In the long goal format of
+ \secref{sec:goals}, term bindings may be included as expected,
+ though.
+
+ \medskip By default, locale specifications are ``closed up'' by
+ turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
+ (modulo local definitions). The predicate statement covers only the
+ newly specified assumptions, omitting the content of included locale
+ expressions. The full cumulative view is only provided on export,
+ involving another predicate \isa{loc} that refers to the complete
+ specification text.
+
+ In any case, the predicate arguments are those locale parameters
+ that actually occur in the respective piece of text. Also note that
+ these predicates operate at the meta-level in theory, but the locale
+ packages attempts to internalize statements according to the
+ object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
+ \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
+ \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
+
+ The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
+ the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
+ constructions. Predicates are also omitted for empty specification
+ texts.
+
+ \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
+ specified locale expression in a flattened form. The notable
+ special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
+ contents of the named locale, but keep in mind that type-inference
+ will normalize type variables according to the usual alphabetical
+ order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
+ Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
+
+ \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
+ of the current theory.
+
+ \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
+ repeatedly expand all introduction rules of locale predicates of the
+ theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
+ assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
+ \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
+ specifications entailed by the context, both from target and
+ \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
+ below). New goals that are entailed by the current context are
+ discharged automatically.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Interpretation of locales%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locale expressions (more precisely, \emph{context expressions}) may
+ be instantiated, and the instantiated facts added to the current
+ context. This requires a proof of the instantiated specification
+ and is called \emph{locale interpretation}. Interpretation is
+ possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\
+ \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+ \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ \indexouternonterm{interp}
+ \begin{rail}
+ 'interpretation' (interp | name ('<' | subseteq) contextexpr)
+ ;
+ 'interpret' interp
+ ;
+ 'print\_interps' '!'? name
+ ;
+ instantiation: ('[' (inst+) ']')?
+ ;
+ interp: thmdecl? \\ (contextexpr instantiation |
+ name instantiation 'where' (thmdecl? prop + 'and'))
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
+
+ The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms
+ \isa{insts} and is positional. All parameters must receive an
+ instantiation term --- with the exception of defined parameters.
+ These are, if omitted, derived from the defining equation and other
+ instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
+
+ The command generates proof obligations for the instantiated
+ specifications (assumes and defines elements). Once these are
+ discharged by the user, instantiated facts are added to the theory
+ in a post-processing phase.
+
+ Additional equations, which are unfolded in facts during
+ post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
+ This is useful for interpreting concepts introduced through
+ definition specification elements. The equations must be proved.
+ Note that if equations are present, the context expression is
+ restricted to a locale name.
+
+ The command is aware of interpretations already active in the
+ theory. No proof obligations are generated for those, neither is
+ post-processing applied to their facts. This avoids duplication of
+ interpreted facts, in particular. Note that, in the case of a
+ locale with import, parts of the interpretation may already be
+ active. The command will only generate proof obligations and
+ process facts for new parts.
+
+ The context expression may be preceded by a name and/or attributes.
+ These take effect in the post-processing of facts. The name is used
+ to prefix fact names, for example to avoid accidental hiding of
+ other facts. Attributes are applied after attributes of the
+ interpreted facts.
+
+ Adding facts to locales has the effect of adding interpreted facts
+ to the theory for all active interpretations also. That is,
+ interpretations dynamically participate in any facts added to
+ locales.
+
+ \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]
+
+ This form of the command interprets \isa{expr} in the locale
+ \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the
+ localized version of the theorem command, the proof is in the
+ context of \isa{name}. After the proof obligation has been
+ dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
+ context \isa{name} is subsequently entered. Note that, like
+ import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
+ Like facts of renamed context elements, facts obtained by
+ interpretation may be accessed by prefixing with the parameter
+ renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
+
+ Unlike interpretation in theories, instantiation is confined to the
+ renaming of parameters, which may be specified as part of the
+ context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
+
+ Only specification fragments of \isa{expr} that are not already
+ part of \isa{name} (be it imported, derived or a derived fragment
+ of the import) are considered by interpretation. This enables
+ circular interpretations.
+
+ If interpretations of \isa{name} exist in the current theory, the
+ command adds interpretations for \isa{expr} as well, with the same
+ prefix and attributes, although only for fragments of \isa{expr}
+ that are not interpreted in the theory already.
+
+ \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
+ interprets \isa{expr} in the proof context and is otherwise
+ similar to interpretation in theories.
+
+ \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
+ interpretations of a particular locale \isa{loc} that are active
+ in the current context, either theory or proof context. The
+ exclamation point argument triggers printing of \emph{witness}
+ theorems justifying interpretations. These are normally omitted
+ from the output.
+
+ \end{descr}
+
+ \begin{warn}
+ Since attributes are applied to interpreted theorems,
+ interpretation may modify the context of common proof tools, e.g.\
+ the Simplifier or Classical Reasoner. Since the behavior of such
+ automated reasoning tools is \emph{not} stable under
+ interpretation morphisms, manual declarations might have to be
+ issued.
+ \end{warn}
+
+ \begin{warn}
+ An interpretation in a theory may subsume previous
+ interpretations. This happens if the same specification fragment
+ is interpreted twice and the instantiation of the second
+ interpretation is more general than the interpretation of the
+ first. A warning is issued, since it is likely that these could
+ have been generalized in the first place. The locale package does
+ not attempt to remove subsumed interpretations.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Classes \label{sec:class}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A class is a particular locale with \emph{exactly one} type variable
+ \isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
+ is established which is interpreted logically as axiomatic type
+ class \cite{Wenzel:1997:TPHOL} whose logical content are the
+ assumptions of the locale. Thus, classes provide the full
+ generality of locales combined with the commodity of type classes
+ (notably type-inference). See \cite{isabelle-classes} for a short
+ tutorial.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+ \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+ \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
+ \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
+ \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
+ \end{matharray}
+
+ \begin{rail}
+ 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
+ 'begin'?
+ ;
+ 'instantiation' (nameref + 'and') '::' arity 'begin'
+ ;
+ 'instance'
+ ;
+ 'subclass' target? nameref
+ ;
+ 'print\_classes'
+ ;
+
+ superclassexpr: nameref | (nameref '+' superclassexpr)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines
+ a new class \isa{c}, inheriting from \isa{superclasses}. This
+ introduces a locale \isa{c} with import of all locales \isa{superclasses}.
+
+ Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
+ theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter
+ \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
+
+ Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
+ mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
+ corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
+ corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
+ --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
+ class membership proofs.
+
+ \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\
+ \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the
+ particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
+ in the target body poses a goal stating these type arities. The
+ target is concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
+
+ Note that a list of simultaneous type constructors may be given;
+ this corresponds nicely to mutual recursive type definitions, e.g.\
+ in Isabelle/HOL.
+
+ \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets
+ up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
+ the type classes involved. After finishing the proof, the
+ background theory will be augmented by the proven type arities.
+
+ \item [\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c}] in a class context for class
+ \isa{d} sets up a goal stating that class \isa{c} is logically
+ contained in class \isa{d}. After finishing the proof, class
+ \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
+
+ \item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
+ theory.
+
+ \item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
+ introduction rules of this theory. Note that this method usually
+ needs not be named explicitly, as it is already included in the
+ default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
+ instantiation of trivial (syntactic) classes may be performed by a
+ single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{The class target%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+%FIXME check
+
+ A named context may refer to a locale (cf.\ \secref{sec:target}).
+ If this locale is also a class \isa{c}, apart from the common
+ locale target behaviour the following happens.
+
+ \begin{itemize}
+
+ \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
+ local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
+ are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
+ referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
+
+ \item Local theorem bindings are lifted as are assumptions.
+
+ \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
+ global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference
+ resolves ambiguities. In rare cases, manual type annotations are
+ needed.
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Axiomatic type classes \label{sec:axclass}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\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}
+ \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
+ \end{matharray}
+
+ Axiomatic type classes are Isabelle/Pure's primitive
+ \emph{definitional} interface to type classes. For practical
+ applications, you should consider using classes
+ (cf.~\secref{sec:classes}) which provide high level interface.
+
+ \begin{rail}
+ 'axclass' classdecl (axmdecl prop +)
+ ;
+ 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of
+ existing classes, with additional axioms holding. Class axioms may
+ not contain more than one type variable. The class axioms (with
+ implicit sort constraints added) are bound to the given names.
+ Furthermore a class introduction rule is generated (being bound as
+ \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
+
+ The ``class axioms'' are stored as theorems according to the given
+ name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
+ the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
+
+ \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
+ \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}]
+ setup a goal stating a class relation or type arity. The proof
+ would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
+ the characteristic theorems of the type classes involved. After
+ finishing the proof, the theory will be augmented by a type
+ signature declaration corresponding to the resulting theorem.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Unrestricted overloading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/Pure's definitional schemes support certain forms of
+ overloading (see \secref{sec:consts}). At most occassions
+ overloading will be used in a Haskell-like fashion together with
+ type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
+ \secref{sec:class}). Sometimes low-level overloading is desirable.
+ The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
+ end-users.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'overloading' \\
+ ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}]
+ opens a theory target (cf.\ \secref{sec:target}) which allows to
+ specify constants with overloaded definitions. These are identified
+ by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type
+ instances. The definitions themselves are established using common
+ specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as
+ reference to the corresponding constants. The target is concluded
+ by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
+
+ A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
+ the corresponding definition, which is occasionally useful for
+ exotic overloading. It is at the discretion of the user to avoid
+ malformed theory specifications!
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Incorporating ML code \label{sec:ML}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+ \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+ \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
+ \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
+ \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}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 [\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML
+ commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
+ down to the ML toplevel and may be modified, using \verb|"Context.>>"| or derived ML commands. The file name is checked with
+ the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
+ header (see also \secref{sec:begin-thy}).
+
+ \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
+
+ \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
+ diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context
+ may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
+ at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
+
+ \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
+ context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
+ of type \verb|"theory -> theory"|. This enables to initialize
+ any object-logic specific tools and packages written in ML, for
+ example.
+
+ \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
+ defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%
+\verb| Proof.context -> Proof.method"|. Parsing concrete method syntax
+ from \verb|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 \isa{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 \verb|Drule.multi_resolves|), while automatic ones just insert the facts
+ using \verb|Method.insert_tac| before applying the main tactic.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Primitive specification elements%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'classes' (classdecl +)
+ ;
+ 'classrel' (nameref ('<' | subseteq) nameref + 'and')
+ ;
+ 'defaultsort' sort
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]
+ declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. Cyclic class structures are not permitted.
+
+ \item [\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states
+ subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and
+ \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \secref{sec:axclass}) provides a way to
+ introduce proven class relations.
+
+ \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{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 [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
+ using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{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 [\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}}]
+ introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}
+ for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. 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 [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]
+ declares a new type constructor \isa{t}, intended as an actual
+ logical type (of the object-logic, if available).
+
+ \item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type
+ constructors \isa{c} (without arguments) to act as purely
+ syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
+ syntax of terms or types.
+
+ \item [\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type
+ constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \S\ref{sec:axclass}) provides a way to
+ introduce proven type arities.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Constants and definitions \label{sec:consts}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Definitions essentially express abbreviations within the logic. The
+ simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
+ where the arguments of \isa{c} appear on the left, abbreviating a
+ prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
+ written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
+ definitions may be weakened by adding arbitrary pre-conditions:
+ \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
+
+ \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 \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} 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 \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
+ recursively at type instances corresponding to the immediate
+ argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
+ specification patterns impose global constraints on all occurrences,
+ e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
+ corresponding occurrences on some right-hand side need to be an
+ instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{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 [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant
+ \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
+ optional mixfix annotations may attach concrete syntax to the
+ constants declared.
+
+ \item [\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn}
+ as a definitional axiom for some existing constant.
+
+ The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} 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 \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} 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 [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{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 ``\isa{{\isacharunderscore}}'' 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 \isa{c} will be \isa{c{\isacharunderscore}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 \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
+ admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
+ particularly useful with locales (see also \S\ref{sec:locale}).
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'axioms' (axmdecl prop +)
+ ;
+ ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] 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 [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
+ 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 [\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}] is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Oracles%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
+ type \verb|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 ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results
+ that are not fully checked by Isabelle inferences.
+
+ \begin{rail}
+ 'oracle' name '(' type ')' '=' text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
+ given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
+ \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
+ ML function of type
+ \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
+ bound to the global identifier \verb|name|.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Name spaces%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{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 [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the
+ current name declaration mode. Initially, theories start in
+ \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically
+ qualified by the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}
+ causes all names to be declared without the theory prefix, until
+ \hyperlink{command.local}{\mbox{\isa{\isacommand{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 [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes
+ declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
+ \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} 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
+ ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Syntax and translations \label{sec:syn-trans}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}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 [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to
+ \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{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 \isa{mode} argument refers to the
+ print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
+ input and output grammar.
+
+ \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
+ grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
+
+ \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic
+ translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
+ parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
+ Translation patterns may be prefixed by the syntactic category to be
+ used for parsing; the default is \isa{logic}.
+
+ \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
+ translation rules, which are interpreted in the same manner as for
+ \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Syntax translation functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}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 \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} 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{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarRef/Thy/document/pure.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/pure.tex Mon Jun 02 22:50:29 2008 +0200
@@ -24,629 +24,6 @@
}
\isamarkuptrue%
%
-\begin{isamarkuptext}%
-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
- ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'', 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Theory commands%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Markup commands \label{sec:markup-thy}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}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 [\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}] mark chapter and
- section headings.
-
- \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}] specifies paragraphs of plain text.
-
- \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}] inserts {\LaTeX} source into the
- output, without additional markup. Thus the full range of document
- manipulations becomes available.
-
- \end{descr}
-
- The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
- \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
- (``antiquotations'', see also \secref{sec:antiq}). These are
- interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
-
- Any of these markup elements corresponds to a {\LaTeX} command with
- the name prefixed by \verb|\isamarkup|. For the sectioning
- commands this is a plain macro with a single argument, e.g.\
- \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
- \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}. The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a
- {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}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 \indexref{}{command}{header}\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration (see \secref{sec:begin-thy}) admits to insert
- section markup just preceding the actual theory definition.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
- \end{matharray}
-
- \begin{rail}
- 'classes' (classdecl +)
- ;
- 'classrel' (nameref ('<' | subseteq) nameref + 'and')
- ;
- 'defaultsort' sort
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]
- declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. Cyclic class structures are not permitted.
-
- \item [\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states
- subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and
- \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \secref{sec:axclass}) provides a way to
- introduce proven class relations.
-
- \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{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 [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
- using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Primitive types and type abbreviations \label{sec:types-pure}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{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 [\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}}]
- introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}
- for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. 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 [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]
- declares a new type constructor \isa{t}, intended as an actual
- logical type (of the object-logic, if available).
-
- \item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type
- constructors \isa{c} (without arguments) to act as purely
- syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
- syntax of terms or types.
-
- \item [\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type
- constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \S\ref{sec:axclass}) provides a way to
- introduce proven type arities.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Primitive constants and definitions \label{sec:consts}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Definitions essentially express abbreviations within the logic. The
- simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
- where the arguments of \isa{c} appear on the left, abbreviating a
- prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
- written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
- definitions may be weakened by adding arbitrary pre-conditions:
- \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
-
- \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 \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} 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 \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
- recursively at type instances corresponding to the immediate
- argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
- specification patterns impose global constraints on all occurrences,
- e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
- corresponding occurrences on some right-hand side need to be an
- instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
-
- \begin{matharray}{rcl}
- \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{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 [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant
- \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
- optional mixfix annotations may attach concrete syntax to the
- constants declared.
-
- \item [\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn}
- as a definitional axiom for some existing constant.
-
- The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} 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 \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} 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 [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{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 ``\isa{{\isacharunderscore}}'' 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 \isa{c} will be \isa{c{\isacharunderscore}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 \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
- admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
- particularly useful with locales (see also \S\ref{sec:locale}).
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Syntax and translations \label{sec:syn-trans}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}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 [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to
- \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{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 \isa{mode} argument refers to the
- print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
- input and output grammar.
-
- \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
- grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
-
- \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic
- translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
- parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
- Translation patterns may be prefixed by the syntactic category to be
- used for parsing; the default is \isa{logic}.
-
- \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
- translation rules, which are interpreted in the same manner as for
- \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Axioms and theorems \label{sec:axms-thms}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- \begin{rail}
- 'axioms' (axmdecl prop +)
- ;
- ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] 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 [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
- 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 [\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}] is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Name spaces%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{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 [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the
- current name declaration mode. Initially, theories start in
- \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically
- qualified by the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}
- causes all names to be declared without the theory prefix, until
- \hyperlink{command.local}{\mbox{\isa{\isacommand{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 [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes
- declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
- \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} 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
- ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Incorporating ML code \label{sec:ML}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
- \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
- \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}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 [\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML
- commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
- down to the ML toplevel and may be modified, using \verb|"Context.>>"| or derived ML commands. The file name is checked with
- the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
- header (see also \secref{sec:begin-thy}).
-
- \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
-
- \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
- diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context
- may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
- at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
-
- \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
- context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
- of type \verb|"theory -> theory"|. This enables to initialize
- any object-logic specific tools and packages written in ML, for
- example.
-
- \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
- defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%
-\verb| Proof.context -> Proof.method"|. Parsing concrete method syntax
- from \verb|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 \isa{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 \verb|Drule.multi_resolves|), while automatic ones just insert the facts
- using \verb|Method.insert_tac| before applying the main tactic.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Syntax translation functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}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 \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} 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{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Oracles%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
- type \verb|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 ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results
- that are not fully checked by Isabelle inferences.
-
- \begin{rail}
- 'oracle' name '(' type ')' '=' text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
- given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
- \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
- ML function of type
- \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
- bound to the global identifier \verb|name|.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Proof commands%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Markup commands \label{sec:markup-prf}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}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}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Other commands%
}
\isamarkuptrue%
@@ -871,15 +248,11 @@
\indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\end{matharray}
\begin{rail}
('cd' | 'use\_thy' | 'update\_thy') name
;
- ('display\_drafts' | 'print\_drafts') (name +)
- ;
\end{rail}
\begin{descr}
@@ -893,11 +266,6 @@
These system commands are scarcely used when working interactively,
since loading of theories is done automatically as required.
- \item [\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{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}%
\end{isamarkuptext}%
\isamarkuptrue%