# HG changeset patch # User wenzelm # Date 971814303 -7200 # Node ID 979336bd0aed2bd7cc8a8011a11c2bba33187306 # Parent 9dc33c6c5df94ca156ded7659c3d68358977cd58 "Deriving rules"; diff -r 9dc33c6c5df9 -r 979336bd0aed doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Tue Oct 17 22:22:56 2000 +0200 +++ b/doc-src/IsarRef/conversion.tex Tue Oct 17 22:25:03 2000 +0200 @@ -154,6 +154,8 @@ \subsection{Goal statements}\label{sec:conv-goal} +\subsubsection{Simple goals} + In ML the canonical a goal statement together with a complete proof script is as follows: \begin{ttbox} @@ -164,7 +166,7 @@ \end{ttbox} This form may be turned into an Isar tactic-emulation script like this: \begin{matharray}{l} - \LEMMA{name}\texttt"{\phi}\texttt" \\ + \LEMMA{name}{\texttt"{\phi}\texttt"} \\ \quad \APPLY{meth@1} \\ \qquad \vdots \\ \quad \DONE \\ @@ -174,20 +176,99 @@ expressions into proof methods. \medskip Classic Isabelle provides many variant forms of goal commands, see -\cite{isabelle-ref} for further details. The second most common one is +also \cite{isabelle-ref} for further details. The second most common one is \texttt{Goalw}, which expands definitions before commencing the actual proof script. \begin{ttbox} Goalw [\(def@1\), \(\dots\)] "\(\phi\)"; \end{ttbox} -This is replaced by using the $unfold$ proof method explicitly. +This may be replaced by using the $unfold$ proof method explicitly. \begin{matharray}{l} -\LEMMA{name}\texttt"{\phi}\texttt" \\ +\LEMMA{name}{\texttt"{\phi}\texttt"} \\ \quad \APPLY{unfold~def@1~\dots} \\ \end{matharray} -%FIXME "goal" and higher-order rules; + +\subsubsection{Deriving rules} + +Deriving non-atomic meta-level propositions requires special precautions in +classic Isabelle: the primitive \texttt{goal} command decomposes a statement +into the atomic conclusion and a list of assumptions, which are exhibited as +ML values of type \texttt{thm}. After the proof is finished, these premises +are discharged again, resulting in the original rule statement. + +In contrast, Isabelle/Isar does \emph{not} require any special treatment of +non-atomic statements --- assumptions and goals may be arbitrarily complex. +While this would basically require to proceed by structured proof, decomposing +the main problem into sub-problems according to the basic Isar scheme of +backward reasoning, the old tactic-style procedure may be mimicked as follows. +The general ML goal statement for derived rules looks like this: +\begin{ttbox} + val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)"; + by \(tac@1\); + \(\vdots\) +\end{ttbox} +This form may be turned into a tactic-emulation script that is wrapped in an +Isar text to get access to the premises as local facts. +\begin{matharray}{l} + \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\ + \PROOF{}~- \\ + \quad \ASSUME{prem@1}{\phi@1}~\AND~\dots \\ + \quad \SHOW{}{\Var{thesis}} \\ + \qquad \APPLY{meth@1} \\ + \qquad\quad \vdots \\ + \qquad \DONE \\ + \QED{} \\ +\end{matharray} +Note that the above scheme repeats the text of premises $\phi@1$, \dots, while +the conclusion $\psi$ is referenced via the automatic text abbreviation +$\Var{thesis}$. The assumption context may be invoked in a less verbose +manner as well, using ``$\CASE{antecedent}$'' instead of +``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above. Then the list of \emph{all} +premises is bound to the name $antecedent$; Isar does not provide a way to +destruct lists into single items, though. +\medskip In practice, actual rules are often rather direct consequences of +corresponding atomic statements, typically stemming from the definition of a +new concept. In that case, the general scheme for deriving rules may be +greatly simplified, using one of the standard automated proof tools, such ad +$simp$, $blast$, or $auto$. This would work as follows: +\begin{matharray}{l} + \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\ + \quad \APPLY{unfold~defs} \quad \CMT{or ``$\APPLY{insert~facts}$''} \\ + \quad \APPLY{blast} \\ + \quad \DONE \\ +\end{matharray} +Note that classic Isabelle would support this form only in the special case +where $\phi@1$, \dots are atomic statements (when using the standard +\texttt{Goal} command). Otherwise the special treatment of rules would be +applied, disturbing this simple setup. + +\medskip Occasionally, derived rules would be established by first proving an +appropriate atomic statement (using $\forall$ and $\longrightarrow$ of the +object-logic), and putting the final result into ``rule format''. In classic +Isabelle this would usually proceed as follows: +\begin{ttbox} + Goal "\(\phi\)"; + by \(tac@1\); + \(\vdots\) + qed_spec_mp "\(name\)"; +\end{ttbox} +The operation performed by \texttt{qed_spec_mp} is also performed by the Isar +attribute ``$rule_format$'', see also \S\ref{sec:rule-format}. Thus the +corresponding Isar text may look like this: +\begin{matharray}{l} + \LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\ + \quad \APPLY{meth@1} \\ + \qquad \vdots \\ + \quad \DONE \\ +\end{matharray} +Note plain ``$rule_format$'' actually performs a slightly different operation: +it fully replaces object-level implication and universal quantification +throughout the whole result statement. This is the right thing in most cases. +For historical reasons, \texttt{qed_spec_mp} would only operate on the +conclusion; one may get this exact behavior by using +``$rule_format~(no_asm)$'' instead. \subsection{Tactics}\label{sec:conv-tac}