# HG changeset patch # User wenzelm # Date 953162915 -3600 # Node ID 80ddf678e53303142157a6013a783ba675ccbb42 # Parent 70fd0b59b0e115a2aef22a5226d45f848bd8ef62 moved "cases" to generic.tex; improved diagnostic commands; history commands; tuned; diff -r 70fd0b59b0e1 -r 80ddf678e533 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Thu Mar 16 00:27:02 2000 +0100 +++ b/doc-src/IsarRef/pure.tex Thu Mar 16 00:28:35 2000 +0100 @@ -137,7 +137,9 @@ argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands may be included here as well. -\medskip Additional markup commands are available for proofs (see +\medskip + +Additional markup commands are available for proofs (see \S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$ declaration (see \S\ref{sec:begin-thy}) admits to insert document markup elements just preceding the actual theory definition. @@ -481,13 +483,11 @@ \subsection{Proof context}\label{sec:proof-context} \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} -\indexisarcmd{case} \begin{matharray}{rcl} \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ \end{matharray} The logical proof context consists of fixed variables and assumptions. The @@ -515,22 +515,6 @@ hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. -\medskip Basically, Isar proof contexts have to be built up explicitly using -any of the above commands. In typical verification tasks this can become hard -to manage, though, with a large number of local contexts emerging from case -analysis or induction, for example. The $\CASENAME$ command provides a -shorthand to refer to certain parts of logical context symbolically. Proof -methods may provide an environment of named ``cases'' of the form $c\colon -\vec x, \vec \chi$. Then the effect of $\CASE{c}$ is exactly the same as -$\FIX{\vec x}~\ASSUME{c}{\vec\chi}$. - -It is important to note that $\CASENAME$ does \emph{not} provide means to peek -at the current goal state, which is considered strictly non-observable in -Isar. Instead, the cases considered here typically emerge in a canonical way -from certain pieces of specification that appears in the theory somewhere, -such as an inductive definition, or recursive function. See -\S\ref{sec:induct-method} for more details of how this works in HOL. - \begin{rail} 'fix' (vars + 'and') comment? ; @@ -538,8 +522,6 @@ ; 'def' thmdecl? \\ var '==' term termpat? comment? ; - 'case' name attributes? - ; var: name ('::' type)? ; @@ -566,9 +548,6 @@ resulting hypothetical equation solved by reflexivity. The default name for the definitional equation is $x_def$. -\item [$\CASE{c}$] invokes local context $c\colon \vec x, \vec \chi$, as - provided by an appropriate proof method. This abbreviates $\FIX{\vec - x}~\ASSUME{c}{\vec\chi}$. \end{descr} The special name $prems$\indexisarthm{prems} refers to all assumptions of the @@ -857,16 +836,16 @@ \subsection{Diagnostics}\label{sec:diag} -\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} -\indexisarcmd{print-facts}\indexisarcmd{print-binds}\indexisarcmd{print-cases} +\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} +\indexisarcmd{print-facts}\indexisarcmd{print-binds} \begin{matharray}{rcl} + \isarcmd{pr} & : & \isarkeep{\cdot} \\ \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\ \isarcmd{term} & : & \isarkeep{theory~|~proof} \\ \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\ \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\ \isarcmd{print_facts} & : & \isarkeep{proof} \\ \isarcmd{print_binds} & : & \isarkeep{proof} \\ - \isarcmd{print_cases} & : & \isarkeep{proof} \\ \end{matharray} These commands are not part of the actual Isabelle/Isar syntax, but assist @@ -874,17 +853,27 @@ theory or proof configuration is not changed. \begin{rail} - 'thm' thmrefs + 'pr' modes? nat? ; - 'term' term + 'thm' modes? thmrefs + ; + 'term' modes? term ; - 'prop' prop + 'prop' modes? prop ; - 'typ' type + 'typ' modes? type + ; + + modes: '(' (name + ) ')' ; \end{rail} \begin{descr} +\item [$\isarkeyword{pr}~n$] prints the current top-level state, i.e.\ the + theory identifier or proof state. The latter includes the proof context, + current facts and goals. The optional argument $n$ affects the implicit + limit of goals to be displayed, which is initially 10. Omitting the limit + leaves the value unchanged. \item [$\isarkeyword{thm}~thms$] retrieves lists of 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 @@ -901,8 +890,56 @@ context, including assumptions and local results. \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in the context. -\item [$\isarkeyword{print_cases}$] prints all local contexts (also known as - ``cases'') of the current goal context. +\end{descr} + +The basic diagnostic commands above admit a list of $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. + +\medskip + +For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would print the +current proof state with mathematical symbols and special characters +represented in {\LaTeX} source, according to the Isabelle style +\cite{isabelle-sys}. The resulting text can be directly pasted into and +\verb,\begin{isabelle},\dots\verb,\end{isabelle}, environment. + +Note that $\isarkeyword{pr}~(latex)$ is sufficient to achieve the same output, +if the current Isabelle session has the other modes already activated, say due +to some particular user interface configuration such as Proof~General +\cite{proofgeneral} with X-Symbol mode \cite{FIXME}. + + +\subsection{History commands}\label{sec:history} + +\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill} +\begin{matharray}{rcl} + \isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\ + \isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\ + \isarcmd{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 +$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be +revoked via $\isarkeyword{redo}$, unless the corresponding the +$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The +$\isarkeyword{kill}$ command aborts the current history node altogether, +discontinuing a proof or even the whole theory. This operation is \emph{not} +undoable. + +\begin{warn} + History commands may not be used with user interfaces such as Proof~General + \cite{proofgeneral}, which takes care of stepping forth and back itself. + Interfering with manual $\isarkeyword{undo}$, $\isarkeyword{redo}$, or even + $\isarkeyword{kill}$ commands would quickly result in utter confusion. +\end{warn} + +\begin{descr} +\item [$\isarkeyword{undo}$] revokes the latest state-transforming command. +\item [$\isarkeyword{redo}$] undos the latest $\isarkeyword{undo}$. +\item [$\isarkeyword{kill}$] aborts the current history level. \end{descr} @@ -928,6 +965,15 @@ macros can be easily adapted to print something like ``$\dots$'' instead of an ``$\OOPS$'' keyword. +\medskip The $\OOPS$ command is undoable, in contrast to $\isarkeyword{kill}$ +(see \S\ref{sec:history}). The effect is to get back to the theory +\emph{before} the opening of the proof. + +\begin{descr} +\item [$\isarkeyword{oops}$] dismisses the current proof, leaving the text in + as properly processed. +\end{descr} + \subsection{System operations} @@ -968,9 +1014,9 @@ \indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{back}\indexisarmeth{tactic} \begin{matharray}{rcl} \isarcmd{apply} & : & \isartrans{proof(prove)}{proof(prove)} \\ - \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{apply_end} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{back} & : & \isartrans{proof}{proof} \\ tactic & : & \isarmeth \\ - \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ \end{matharray} \railalias{applyend}{apply\_end} @@ -983,8 +1029,6 @@ ; 'tactic' text ; - 'back' - ; \end{rail} \begin{descr} @@ -1004,24 +1048,25 @@ No facts are passed to $m$. Furthermore, the static context is that of the enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not refer to any assumptions introduced in the current body, for example. +\item [$\isarkeyword{back}$] does back-tracking over the result sequence of + the latest proof command.\footnote{Unlike the ML function \texttt{back} + \cite{isabelle-ref}, the Isar command does not search upwards for further + branch points.} Basically, any proof command may return multiple results. \item [$tactic~text$] produces a proof method from any ML text of type \texttt{tactic}. Apart from the usual ML environment, and the current implicit theory context, the ML code may refer to the following locally bound values: - \begin{ttbox} +%%FIXME ttbox produces too much trailing space +{\footnotesize\begin{verbatim} val ctxt : Proof.context val facts : thm list val thm : string -> thm val thms : string -> thm list - \end{ttbox} +\end{verbatim}} Here \texttt{ctxt} refers to the current proof context, \texttt{facts} indicates any current facts for forward-chaining, and \texttt{thm}~/~\texttt{thms} retrieve named facts (including global theorems) from the context. -\item [$\isarkeyword{back}$] does back-tracking over the result sequence of - the latest proof command.\footnote{Unlike the ML function \texttt{back} - \cite{isabelle-ref}, the Isar command does not search upwards for further - branch points.} Basically, any proof command may return multiple results. \end{descr}