# HG changeset patch # User wenzelm # Date 953402867 -3600 # Node ID 160739e1f44350ecd2f5b376dc5420347c86e255 # Parent b6497971acbf7126e7b44d96db3ced810ee98875 pure methods / atts moved here; tactic emulation moved here; oops moved here; history commands; tuned; diff -r b6497971acbf -r 160739e1f443 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Sat Mar 18 19:04:32 2000 +0100 +++ b/doc-src/IsarRef/pure.tex Sat Mar 18 19:07:47 2000 +0100 @@ -1,12 +1,12 @@ \chapter{Basic Isar Language Elements}\label{ch:pure-syntax} -Subsequently, we introduce the main part of the basic Isar theory and proof -commands as provided by Isabelle/Pure. Chapter~\ref{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-loaded by most object -logics. Chapter~\ref{ch:hol-tools} refers to actual object-logic specific -elements of Isabelle/HOL. +Subsequently, we introduce the main part of Pure Isar theory and proof +commands, together with a few fundamental proof methods and attributes. +Chapter~\ref{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 by most object logics. Chapter~\ref{ch:hol-tools} +refers to actual object-logic specific elements of Isabelle/HOL. \medskip @@ -532,12 +532,13 @@ \end{rail} \begin{descr} -\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$. -\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems - $\Phi$ by assumption. Subsequent results applied to an enclosing goal - (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be - able to unify with existing premises in the goal, while $\PRESUMENAME$ - leaves $\Phi$ as new subgoals. +\item [$\FIX{\vec x}$] introduces a local \emph{arbitrary, but fixed} + variables $\vec x$. +\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local + theorems $\vec\phi$ by assumption. Subsequent results applied to an + enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ + expects to be able to unify with existing premises in the goal, while + $\PRESUMENAME$ leaves $\vec\phi$ as new subgoals. Several lists of assumptions may be given (separated by $\isarkeyword{and}$); the resulting list of current facts consists of all of @@ -586,7 +587,7 @@ establish the goal to be claimed next. The initial proof method invoked to refine that will be offered the facts to do ``anything appropriate'' (cf.\ also \S\ref{sec:proof-steps}). For example, method $rule$ (see - \S\ref{sec:pure-meth}) would typically do an elimination rather than an + \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an introduction. Automatic methods usually insert the facts into the goal state before operation. \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is @@ -595,12 +596,12 @@ chaining is from earlier facts together with the current ones. \end{descr} -Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect +Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect multiple facts to be given in their proper order, corresponding to a prefix of the premises of the rule involved. Note that positions may be easily skipped using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves -the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure -as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} +the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be bound in +Isabelle/Pure as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} \subsection{Goal statements} @@ -683,10 +684,6 @@ automatic proof tools that are prone leave a large number of badly structured sub-goals are no help in continuing the proof document in any intelligible way. -%FIXME -%A more appropriate technique would be to $\SHOWNAME$ some non-trivial -%reduction as an explicit rule, which is solved completely by some automated -%method, and then applied to some pending goal. \medskip @@ -729,15 +726,90 @@ by expanding its definition; in many cases $\PROOF{m@1}$ is already sufficient to see what is going wrong. \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it - abbreviates $\BY{default}$. + abbreviates $\BY{rule}$. \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it abbreviates $\BY{this}$. \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the \texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the - goal without further ado. Of course, the result is a fake theorem only, - involving some oracle in its internal derivation object (this is indicated - as ``$[!]$'' in the printed result). The main application of $\SORRY$ is to - support experimentation and top-down proof development. + goal without further ado. Of course, the result would be a fake theorem + only, involving some oracle in its internal derivation object (this is + indicated as ``$[!]$'' in the printed result). The main application of + $\SORRY$ is to support experimentation and top-down proof development. +\end{descr} + + +\subsection{Fundamental methods and attributes}\label{sec:pure-meth-att} + +The following proof methods and attributes refer to some basic logical +operations of Isar. Further methods and attributes are provided by several +generic and object-logic specific tools and packages (see chapters +\ref{ch:gen-tools} and \ref{ch:hol-tools}). + +\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$} +\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} +\indexisaratt{OF}\indexisaratt{of} +\begin{matharray}{rcl} + assumption & : & \isarmeth \\ + this & : & \isarmeth \\ + rule & : & \isarmeth \\ + - & : & \isarmeth \\ + OF & : & \isaratt \\ + of & : & \isaratt \\ + intro & : & \isaratt \\ + elim & : & \isaratt \\ + dest & : & \isaratt \\ + delrule & : & \isaratt \\ +\end{matharray} + +\begin{rail} + 'rule' thmrefs + ; + 'OF' thmrefs + ; + 'of' (inst * ) ('concl' ':' (inst * ))? + ; + + inst: underscore | term + ; +\end{rail} + +\begin{descr} +\item [$assumption$] solves some goal by a single assumption step. Any facts + given (${} \le 1$) are guaranteed to participate in the refinement. Recall + that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any + remaining sub-goals by assumption. +\item [$this$] applies all of the current facts directly as rules. Recall + that ``$\DOT$'' (dot) abbreviates $\BY{this}$. +\item [$rule~thms$] applies some rule given as argument in backward manner; + facts are used to reduce the rule before applying it to the goal. Thus + $rule$ without facts is plain \emph{introduction}, while with facts it + becomes \emph{elimination}. + + When omitting the $thms$ argument, the $rule$ method tries to pick + appropriate rules automatically, as declared in the current context using + the $intro$, $elim$, $dest$ attributes (see below). This is the default + behavior of $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see + \S\ref{sec:proof-steps}). +\item [``$-$''] does nothing but insert the forward chaining facts as premises + into the goal. Note that command $\PROOFNAME$ without any method actually + performs a single reduction step using the $rule$ method; thus a plain + \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$ + alone. +\item [$OF~thms$] applies $thms$ in parallel (cf.\ \texttt{MRS} in + \cite[\S5]{isabelle-ref}, but note the reversed order). Some premises may + be skipped by including ``$\_$'' (underscore) as argument. +\item [$of~ts$] performs positional instantiation. The terms $ts$ are + substituted for any schematic variables occurring in a theorem from left to + right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments + following a ``$concl\colon$'' specification refer to positions of the + conclusion of a rule. +\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and + destruct rules, respectively. Note that the classical reasoner (see + \S\ref{sec:classical-basic}) introduces different versions of these + attributes, and the $rule$ method, too. In object-logics with classical + reasoning enabled, the latter version should be used all the time to avoid + confusion! +\item [$delrule$] undeclares introduction or elimination rules. \end{descr} @@ -832,6 +904,117 @@ \end{descr} +\subsection{Emulating tactic scripts} + +The following elements emulate unstructured tactic scripts to some extent. +While these are anathema for writing proper Isar proof documents, they might +come in handy for interactive exploration and debugging, or even actual +tactical proof within new-style theories (to benefit from document +preparation, for example). + +\indexisarcmd{apply}\indexisarcmd{apply-end} +\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} +\indexisarmeth{tactic} +\begin{matharray}{rcl} + \isarcmd{apply} & : & \isartrans{proof(prove)}{proof(prove)} \\ + \isarcmd{apply_end} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{defer} & : & \isartrans{proof}{proof} \\ + \isarcmd{prefer} & : & \isartrans{proof}{proof} \\ + \isarcmd{back} & : & \isartrans{proof}{proof} \\ + tactic & : & \isarmeth \\ +\end{matharray} + +\railalias{applyend}{apply\_end} +\railterm{applyend} + +\begin{rail} + 'apply' method + ; + applyend method + ; + 'defer' nat? + ; + 'prefer' nat + ; + 'tactic' text + ; +\end{rail} + +\begin{descr} +\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in an initial + position, but retains ``$prove$'' mode (unlike $\PROOFNAME$). Thus + consecutive method applications may be given just as in tactic scripts. In + order to complete the proof properly, any of the actual structured proof + commands (e.g.\ ``$\DOT$'') has to be given eventually. + + Facts are passed to $m$ as indicated by the goal's forward-chain mode. + Common use of $\isarkeyword{apply}$ would be in a purely backward manner, + though. +\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in + terminal position. Basically, this simulates a multi-step tactic script for + $\QEDNAME$, but may be given anywhere within the proof body. + + 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{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list + of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ + by default), while $prefer$ brings goal $n$ to the top. +\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: +%%FIXME ttbox produces too much trailing space (why?) +{\footnotesize\begin{verbatim} +val ctxt : Proof.context +val facts : thm list +val thm : string -> thm +val thms : string -> thm list +\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. +\end{descr} + + +\subsection{Meta-linguistic features} + +\indexisarcmd{oops} +\begin{matharray}{rcl} + \isarcmd{oops} & : & \isartrans{proof}{theory} \\ +\end{matharray} + +The $\OOPS$ command discontinues the current proof attempt, while considering +the partial proof text as properly processed. This is conceptually quite +different from ``faking'' actual proofs via $\SORRY$ (see +\S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all, +but goes back right to the theory level. Furthermore, $\OOPS$ does not +produce any result theorem --- there is no claim to be able to complete the +proof anyhow. + +A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the +system itself, in conjunction with the document preparation tools of Isabelle +described in \cite{isabelle-sys}. Thus partial or even wrong proof attempts +can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} +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. + +%FIXME remove +% \begin{descr} +% \item [$\isarkeyword{oops}$] dismisses the current proof, leaving the text in +% as properly processed. +% \end{descr} + + \section{Other commands} \subsection{Diagnostics}\label{sec:diag} @@ -839,13 +1022,14 @@ \indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ} \indexisarcmd{print-facts}\indexisarcmd{print-binds} \begin{matharray}{rcl} - \isarcmd{pr} & : & \isarkeep{theory~|~proof} \\ - \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{help}^* & : & \isarkeep{\cdot} \\ + \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} \\ \end{matharray} These commands are not part of the actual Isabelle/Isar syntax, but assist @@ -869,6 +1053,8 @@ \end{rail} \begin{descr} +\item [$\isarkeyword{help}$] prints a list of available language elements. + Note that methods and attributes depend on the current theory context. \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 @@ -937,43 +1123,12 @@ 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} - - -\subsection{Meta-linguistic features} - -\indexisarcmd{oops} -\begin{matharray}{rcl} - \isarcmd{oops}^* & : & \isartrans{proof}{theory} \\ -\end{matharray} - -The $\OOPS$ command discontinues the current proof attempt, while considering -the partial proof text as properly processed. This is conceptually quite -different from ``faking'' actual proofs via $\SORRY$ (see -\S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all, -but goes back right to the theory level. Furthermore, $\OOPS$ does not -produce any result theorem --- there is no claim to be able to complete the -proof anyhow. - -A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the -system itself, in conjunction with the document preparation tools of Isabelle -described in \cite{isabelle-sys}. Thus partial or even wrong proof attempts -can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} -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} +%FIXME remove +% \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} \subsection{System operations} @@ -981,12 +1136,12 @@ \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only} \indexisarcmd{update-thy}\indexisarcmd{update-thy-only} \begin{matharray}{rcl} - \isarcmd{cd} & : & \isarkeep{\cdot} \\ - \isarcmd{pwd} & : & \isarkeep{\cdot} \\ - \isarcmd{use_thy} & : & \isarkeep{\cdot} \\ - \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\ - \isarcmd{update_thy} & : & \isarkeep{\cdot} \\ - \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\ + \isarcmd{cd}^* & : & \isarkeep{\cdot} \\ + \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\ + \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\ + \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\ + \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\ + \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\ \end{matharray} \begin{descr} @@ -1006,82 +1161,6 @@ interface, since loading of theories is done fully transparently. -\subsection{Emulating tactic scripts} - -The following elements emulate unstructured tactic scripts to some extent. -While these are anathema for writing proper Isar proof documents, they might -come in handy for interactive exploration and debugging. - -\indexisarcmd{apply}\indexisarcmd{apply-end} -\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} -\indexisarmeth{tactic} -\begin{matharray}{rcl} - \isarcmd{apply} & : & \isartrans{proof(prove)}{proof(prove)} \\ - \isarcmd{apply_end} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{defer} & : & \isartrans{proof}{proof} \\ - \isarcmd{prefer} & : & \isartrans{proof}{proof} \\ - \isarcmd{back} & : & \isartrans{proof}{proof} \\ - tactic & : & \isarmeth \\ -\end{matharray} - -\railalias{applyend}{apply\_end} -\railterm{applyend} - -\begin{rail} - 'apply' method - ; - applyend method - ; - 'defer' nat? - ; - 'prefer' nat - ; - 'tactic' text - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in an initial - position, but retains ``$prove$'' mode (unlike $\PROOFNAME$). Thus - consecutive method applications may be given just as in tactic scripts. In - order to complete the proof properly, any of the actual structured proof - commands (e.g.\ ``$\DOT$'') has to be given eventually. - - Facts are passed to $m$ as indicated by the goal's forward-chain mode. - Common use of $\isarkeyword{apply}$ would be in a purely backward manner, - though. -\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in - terminal position. Basically, this simulates a multi-step tactic script for - $\QEDNAME$, but may be given anywhere within the proof body. - - 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{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list - of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ - by default), while $prefer$ brings goal $n$ to the top. -\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: -%%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{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. -\end{descr} - - %%% Local Variables: %%% mode: latex %%% TeX-master: "isar-ref"