# HG changeset patch # User wenzelm # Date 1212442708 -7200 # Node ID 5c48cecb981b663cd3d0d0a443e0e3fbd276e5b9 # Parent a53dfe9096748898c5251981580a88e37c453af9 updated generated file; diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Jun 02 23:38:27 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Jun 02 23:38:28 2008 +0200 @@ -78,6 +78,7 @@ % \begin{isamarkuptext}% \begin{matharray}{rcl} + \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\[0.5ex] \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} \\ @@ -99,12 +100,17 @@ \begin{rail} ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text ; - ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text + ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text ; \end{rail} \begin{descr} + \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} for further markup commands. + \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. diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/Introduction.tex --- a/doc-src/IsarRef/Thy/document/Introduction.tex Mon Jun 02 23:38:27 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/Introduction.tex Mon Jun 02 23:38:28 2008 +0200 @@ -11,7 +11,7 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ Introduction\isanewline -\isakeyword{imports}\ Pure\isanewline +\isakeyword{imports}\ Main\isanewline \isakeyword{begin}% \endisatagtheory {\isafoldtheory}% @@ -92,7 +92,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Quick start% +\isamarkupsection{User interfaces% } \isamarkuptrue% % @@ -255,7 +255,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}% +\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}% } \isamarkuptrue% % diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/Misc.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/document/Misc.tex Mon Jun 02 23:38:28 2008 +0200 @@ -0,0 +1,287 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Misc}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Misc\isanewline +\isakeyword{imports}\ Main\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Other commands \label{ch:pure-syntax}% +} +\isamarkuptrue% +% +\isamarkupsection{Diagnostics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + These diagnostic commands assist interactive development. Note that + \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof + configuration is not changed. + + \begin{rail} + 'pr' modes? nat? (',' nat)? + ; + 'thm' modes? thmrefs + ; + 'term' modes? term + ; + 'prop' modes? prop + ; + 'typ' modes? type + ; + 'prf' modes? thmrefs? + ; + 'full\_prf' modes? thmrefs? + ; + + modes: '(' (name + ) ')' + ; + \end{rail} + + \begin{descr} + + \item [\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current + proof state (if present), including the proof context, current facts + and goals. The optional limit arguments affect the number of goals + and premises to be displayed, which is initially 10 for both. + Omitting limit values leaves the current setting unchanged. + + \item [\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves + theorems from the current theory or proof context. Note that any + attributes included in the theorem specifications are applied to a + temporary context derived from the current theory or proof; the + result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect. + + \item [\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}] + read, type-check and print terms or propositions according to the + current theory or proof context; the inferred type of \isa{t} is + output as well. Note that these commands are also useful in + inspecting the current environment of term abbreviations. + + \item [\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}}] reads and prints types of the + meta-logic according to the current theory or proof context. + + \item [\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}] displays the (compact) proof term of the + current proof state (if present), or of the given theorems. 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 [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays + the full proof term, i.e.\ also displays information omitted in the + compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders + there. + + \end{descr} + + All of the diagnostic commands above admit a list of \isa{modes} + to be specified, which is appended to the current print mode (see + also \cite{isabelle-ref}). Thus the output behavior may be modified + according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}{\isachardoublequote}} would print the current + proof state with mathematical symbols and special characters + represented in {\LaTeX} source, according to the Isabelle style + \cite{isabelle-sys}. + + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more + systematic way to include formal items into the printed text + document.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Inspecting the context% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ + \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ + \end{matharray} + + \begin{rail} + 'print\_theory' ( '!'?) + ; + + 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) + ; + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | + 'simp' ':' term | term) + ; + 'thm\_deps' thmrefs + ; + \end{rail} + + These commands print certain parts of the theory and proof context. + Note that there are some further ones available, such as for the set + of rules declared for simplifications. + + \begin{descr} + + \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory + syntax, including keywords and command. + + \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of + the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra + verbosity. + + \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types + and terms, depending on the current context. The output can be very + verbose, including grammar tables and syntax translation rules. See + \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's + inner syntax. + + \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods + available in the current theory context. + + \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes + available in the current theory context. + + \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from + the last command. + + \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts + from the theory or proof context matching all of given search + criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems + whose fully qualified name matches pattern \isa{p}, which may + contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro}, + \isa{elim}, and \isa{dest} select theorems that match the + current goal as introduction, elimination or destruction rules, + respectively. The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite + rules whose left-hand side matches the given term. The criterion + term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy + ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints. + + Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that + do \emph{not} match. Note that giving the empty list of criteria + yields \emph{all} currently known facts. An optional limit for the + number of printed facts may be given; the default is 40. By + default, duplicates are removed from the search result. Use + \isa{with{\isacharunderscore}dups} to display duplicates. + + \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] + visualizes dependencies of facts, using Isabelle's graph browser + tool (see also \cite{isabelle-sys}). + + \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the + current context, both named and unnamed ones. + + \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations + present in the context. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{History commands \label{sec:history}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \end{matharray} + + The Isabelle/Isar top-level maintains a two-stage history, for + theory and proof state transformation. Basically, any command can + be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic + elements. Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless + the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning + of a proof or theory. The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the + current history node altogether, discontinuing a proof or even the + whole theory. This operation is \emph{not} undo-able. + + \begin{warn} + History commands should never be used with user interfaces such as + Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes + care of stepping forth and back itself. Interfering by manual + \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} + commands would quickly result in utter confusion. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{System operations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \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} \\ + \end{matharray} + + \begin{rail} + ('cd' | 'use\_thy' | 'update\_thy') name + ; + \end{rail} + + \begin{descr} + + \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory + of the Isabelle process. + + \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory. + + \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}. + These system commands are scarcely used when working interactively, + since loading of theories is done automatically as required. + + \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: diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/Outer_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Jun 02 23:38:27 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Jun 02 23:38:28 2008 +0200 @@ -11,7 +11,7 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ Outer{\isacharunderscore}Syntax\isanewline -\isakeyword{imports}\ Pure\isanewline +\isakeyword{imports}\ Main\isanewline \isakeyword{begin}% \endisatagtheory {\isafoldtheory}% diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Jun 02 23:38:27 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Jun 02 23:38:28 2008 +0200 @@ -30,7 +30,6 @@ % \begin{isamarkuptext}% \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{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\ \end{matharray} @@ -45,14 +44,10 @@ 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} 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. + pre-theory markup command (cf.\ \secref{sec:markup}). 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 - ; 'theory' name 'imports' (name +) uses? 'begin' ; @@ -61,11 +56,6 @@ \begin{descr} - \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} 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}}. @@ -121,9 +111,9 @@ \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. + class definitions allow to include the \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 diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/pure.tex --- a/doc-src/IsarRef/Thy/document/pure.tex Mon Jun 02 23:38:27 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,291 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{pure}% -% -\isadelimtheory -\isanewline -\isanewline -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ pure\isanewline -\isakeyword{imports}\ Pure\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupchapter{Basic language elements \label{ch:pure-syntax}% -} -\isamarkuptrue% -% -\isamarkupsection{Other commands% -} -\isamarkuptrue% -% -\isamarkupsubsection{Diagnostics% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcl} - \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ - \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \end{matharray} - - These diagnostic commands assist interactive development. Note that - \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof - configuration is not changed. - - \begin{rail} - 'pr' modes? nat? (',' nat)? - ; - 'thm' modes? thmrefs - ; - 'term' modes? term - ; - 'prop' modes? prop - ; - 'typ' modes? type - ; - 'prf' modes? thmrefs? - ; - 'full\_prf' modes? thmrefs? - ; - - modes: '(' (name + ) ')' - ; - \end{rail} - - \begin{descr} - - \item [\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current - proof state (if present), including the proof context, current facts - and goals. The optional limit arguments affect the number of goals - and premises to be displayed, which is initially 10 for both. - Omitting limit values leaves the current setting unchanged. - - \item [\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves - theorems from the current theory or proof context. Note that any - attributes included in the theorem specifications are applied to a - temporary context derived from the current theory or proof; the - result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect. - - \item [\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}] - read, type-check and print terms or propositions according to the - current theory or proof context; the inferred type of \isa{t} is - output as well. Note that these commands are also useful in - inspecting the current environment of term abbreviations. - - \item [\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}}] reads and prints types of the - meta-logic according to the current theory or proof context. - - \item [\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}] displays the (compact) proof term of the - current proof state (if present), or of the given theorems. 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 [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays - the full proof term, i.e.\ also displays information omitted in the - compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders - there. - - \end{descr} - - All of the diagnostic commands above admit a list of \isa{modes} - to be specified, which is appended to the current print mode (see - also \cite{isabelle-ref}). Thus the output behavior may be modified - according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}{\isachardoublequote}} would print the current - proof state with mathematical symbols and special characters - represented in {\LaTeX} source, according to the Isabelle style - \cite{isabelle-sys}. - - Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more - systematic way to include formal items into the printed text - document.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Inspecting the context% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcl} - \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ - \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ - \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ - \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ - \end{matharray} - - \begin{rail} - 'print\_theory' ( '!'?) - ; - - 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) - ; - criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | - 'simp' ':' term | term) - ; - 'thm\_deps' thmrefs - ; - \end{rail} - - These commands print certain parts of the theory and proof context. - Note that there are some further ones available, such as for the set - of rules declared for simplifications. - - \begin{descr} - - \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory - syntax, including keywords and command. - - \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of - the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra - verbosity. - - \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types - and terms, depending on the current context. The output can be very - verbose, including grammar tables and syntax translation rules. See - \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's - inner syntax. - - \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods - available in the current theory context. - - \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes - available in the current theory context. - - \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from - the last command. - - \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts - from the theory or proof context matching all of given search - criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems - whose fully qualified name matches pattern \isa{p}, which may - contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro}, - \isa{elim}, and \isa{dest} select theorems that match the - current goal as introduction, elimination or destruction rules, - respectively. The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite - rules whose left-hand side matches the given term. The criterion - term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy - ``\isa{{\isacharunderscore}}'', schematic variables, and type constraints. - - Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that - do \emph{not} match. Note that giving the empty list of criteria - yields \emph{all} currently known facts. An optional limit for the - number of printed facts may be given; the default is 40. By - default, duplicates are removed from the search result. Use - \isa{with{\isacharunderscore}dups} to display duplicates. - - \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] - visualizes dependencies of facts, using Isabelle's graph browser - tool (see also \cite{isabelle-sys}). - - \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the - current context, both named and unnamed ones. - - \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations - present in the context. - - \end{descr}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{History commands \label{sec:history}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcl} - \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ - \indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ - \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ - \end{matharray} - - The Isabelle/Isar top-level maintains a two-stage history, for - theory and proof state transformation. Basically, any command can - be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic - elements. Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless - the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning - of a proof or theory. The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the - current history node altogether, discontinuing a proof or even the - whole theory. This operation is \emph{not} undo-able. - - \begin{warn} - History commands should never be used with user interfaces such as - Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes - care of stepping forth and back itself. Interfering by manual - \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} - commands would quickly result in utter confusion. - \end{warn}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{System operations% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcl} - \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} \\ - \end{matharray} - - \begin{rail} - ('cd' | 'use\_thy' | 'update\_thy') name - ; - \end{rail} - - \begin{descr} - - \item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory - of the Isabelle process. - - \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory. - - \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}. - These system commands are scarcely used when working interactively, - since loading of theories is done automatically as required. - - \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: