# HG changeset patch # User wenzelm # Date 966271652 -7200 # Node ID 60d8c954390fcd18bfd1998449bd3cc412b9308b # Parent abe51fcb222205b178382be8cb792b6069a2031e added 'declare' command; moved tactic emulations; tuned; renamed "res_inst_tac' etc. to 'rule_tac' etc.; tuned; diff -r abe51fcb2222 -r 60d8c954390f doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Mon Aug 14 18:45:49 2000 +0200 +++ b/doc-src/IsarRef/pure.tex Mon Aug 14 18:47:32 2000 +0200 @@ -292,7 +292,7 @@ \end{descr} -\subsection{Axioms and theorems} +\subsection{Axioms and theorems}\label{sec:axms-thms} \indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas} \begin{matharray}{rcl} @@ -430,8 +430,8 @@ {\footnotesize \begin{verbatim} -Method.no_args (Method.METHOD (fn facts => foobar_tac)) -Method.thms_args (fn thms => (Method.METHOD (fn facts => foobar_tac))) + Method.no_args (Method.METHOD (fn facts => foobar_tac)) + Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) \end{verbatim} } @@ -1026,41 +1026,45 @@ \end{descr} -\subsection{Emulating tactic scripts}\label{sec:tactical-proof} +\subsection{Emulating tactic scripts}\label{sec:tactic-commands} -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). +The Isar provides separate commands to accommodate tactic-style proof scripts +within the same system. While being outside the orthodox Isar proof language, +these 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). See also \S\ref{sec:tactics} for actual tactics, +that have been encapsulated as proof methods. Proper proof methods may be +used in scripts, too. -\indexisarcmd{apply}\indexisarcmd{done}\indexisarcmd{apply-end} +\indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done} \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} +\indexisarcmd{declare} \begin{matharray}{rcl} \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ + \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ - \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ + \isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ \end{matharray} \railalias{applyend}{apply\_end} \railterm{applyend} \begin{rail} - 'apply' method comment? + ( 'apply' | applyend ) method comment? ; 'done' comment? ; - applyend method comment? - ; 'defer' nat? comment? ; 'prefer' nat comment? ; 'back' comment? ; + 'declare' thmrefs comment? + ; \end{rail} \begin{descr} @@ -1072,11 +1076,6 @@ are \emph{consumed} afterwards. Thus any further $\isarkeyword{apply}$ command would always work in a purely backward manner. -\item [$\isarkeyword{done}$] completes a proof script, provided that the - current goal state is already solved completely. Note that actual - structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to - conclude proof scripts as well. - \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. @@ -1084,13 +1083,26 @@ 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{done}$] completes a proof script, provided that the + current goal state is already solved completely. Note that actual + structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to + conclude proof scripts as well. + \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 [$\isarkeyword{declare}~thms$] declares theorems to the current theory + context. No theorem binding is involved here, unlike + $\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ + \S\ref{sec:axms-thms}). So $\isarkeyword{declare}$ only has the effect of + applying attributes as included in the theorem specification. \end{descr} Any proper Isar proof method may be used with tactic script commands such as @@ -1098,82 +1110,6 @@ provided as well; these would be never used in actual structured proofs, of course. -\indexisarmeth{tactic}\indexisarmeth{insert} -\indexisarmeth{res-inst-tac}\indexisarmeth{eres-inst-tac} -\indexisarmeth{dres-inst-tac}\indexisarmeth{forw-inst-tac} -\indexisarmeth{subgoal-tac} -\begin{matharray}{rcl} - tactic^* & : & \isarmeth \\ - insert^* & : & \isarmeth \\ - res_inst_tac^* & : & \isarmeth \\ - eres_inst_tac^* & : & \isarmeth \\ - dres_inst_tac^* & : & \isarmeth \\ - forw_inst_tac^* & : & \isarmeth \\ - subgoal_tac^* & : & \isarmeth \\ -\end{matharray} - -\railalias{resinsttac}{res\_inst\_tac} -\railterm{resinsttac} - -\railalias{eresinsttac}{eres\_inst\_tac} -\railterm{eresinsttac} - -\railalias{dresinsttac}{dres\_inst\_tac} -\railterm{dresinsttac} - -\railalias{forwinsttac}{forw\_inst\_tac} -\railterm{forwinsttac} - -\railalias{subgoaltac}{subgoal\_tac} -\railterm{subgoaltac} - -\begin{rail} - 'tactic' text - ; - 'insert' thmrefs - ; - ( resinsttac | eresinsttac | dresinsttac | forwinsttac ) goalspec? \\ - ((name '=' term) + 'and') 'in' thmref - ; - subgoaltac goalspec? prop - ; -\end{rail} - -\begin{descr} -\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. -\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof - state; the current facts indicated for forward chaining are ignored! -\item [$res_inst_tac$ etc.] do resolution of rules with explicit - instantiation. This works the same way as the corresponding ML tactics, see - \cite[\S3]{isabelle-ref}. - - It is very important to note that the instantiations are read and - type-checked according to the dynamic goal state, rather than the static - proof context! In particular, locally fixed variables and term - abbreviations may not be included in the term specifications. -\item [$subgoal_tac~\phi$] emulates the ML tactic of the same name, see - \cite[\S3]{isabelle-ref}. Syntactically, the given proposition is handled - as the instantiations in $res_inst_tac$ etc. - - Note that the proper Isar command $\PRESUMENAME$ achieves a similar effect - as $subgoal_tac$. -\end{descr} - \subsection{Meta-linguistic features} @@ -1204,23 +1140,19 @@ \section{Other commands} -\subsection{Diagnostics}\label{sec:diag} +\subsection{Diagnostics} \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} \\ \end{matharray} -These commands are not part of the actual Isabelle/Isar syntax, but assist -interactive development. Also note that $undo$ does not apply here, since the -theory or proof configuration is not changed. +These diagnostic commands assist interactive development. Note that $undo$ +does not apply here, the theory or proof configuration is not changed. \begin{rail} 'pr' modes? nat? @@ -1255,27 +1187,55 @@ abbreviations. \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic according to the current theory or proof context. +\end{descr} + +All of the 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. 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}. + +Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic +way to include formal items into the printed text document. + + +\subsection{Inspecting the context} + +\indexisarcmd{print-facts}\indexisarcmd{print-binds} +\indexisarcmd{print-commands}\indexisarcmd{print-syntax} +\indexisarcmd{print-methods}\indexisarcmd{print-attributes} +\begin{matharray}{rcl} + \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ + \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{print_facts}^* & : & \isarkeep{proof} \\ + \isarcmd{print_binds}^* & : & \isarkeep{proof} \\ +\end{matharray} + +These commands print 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 [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, + including keywords and command. +\item [$\isarkeyword{print_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 [$\isarkeyword{print_methods}$] all proof methods available in the + current theory context. +\item [$\isarkeyword{print_attributes}$] all attributes available in the + current theory context. \item [$\isarkeyword{print_facts}$] prints any named facts of the current context, including assumptions and local results. \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in the 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. - -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 a -\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,Aspinall:TACAS:2000} with X-Symbol mode \cite{x-symbol}. - \subsection{History commands}\label{sec:history}