improved ``deriving rules'';
authorwenzelm
Mon Mar 04 19:07:22 2002 +0100 (2002-03-04)
changeset 130134db07fc3d96f
parent 13012 f8bfc61ee1b5
child 13014 3c1c493e6d93
improved ``deriving rules'';
doc-src/IsarRef/conversion.tex
     1.1 --- a/doc-src/IsarRef/conversion.tex	Mon Mar 04 19:06:52 2002 +0100
     1.2 +++ b/doc-src/IsarRef/conversion.tex	Mon Mar 04 19:07:22 2002 +0100
     1.3 @@ -171,9 +171,9 @@
     1.4    \qquad \vdots \\
     1.5    \quad \DONE \\
     1.6  \end{matharray}
     1.7 -Note that the main statement may be $\THEOREMNAME$ as well.  See
     1.8 -\S\ref{sec:conv-tac} for further details on how to convert actual tactic
     1.9 -expressions into proof methods.
    1.10 +Note that the main statement may be $\THEOREMNAME$ or $\COROLLARYNAME$ as
    1.11 +well.  See \S\ref{sec:conv-tac} for further details on how to convert actual
    1.12 +tactic expressions into proof methods.
    1.13  
    1.14  \medskip Classic Isabelle provides many variant forms of goal commands, see
    1.15  also \cite{isabelle-ref} for further details.  The second most common one is
    1.16 @@ -195,38 +195,24 @@
    1.17  classic Isabelle: the primitive \texttt{goal} command decomposes a statement
    1.18  into the atomic conclusion and a list of assumptions, which are exhibited as
    1.19  ML values of type \texttt{thm}.  After the proof is finished, these premises
    1.20 -are discharged again, resulting in the original rule statement.
    1.21 -
    1.22 -In contrast, Isabelle/Isar does \emph{not} require any special treatment of
    1.23 -non-atomic statements --- assumptions and goals may be arbitrarily complex.
    1.24 -While this would basically require to proceed by structured proof, decomposing
    1.25 -the main problem into sub-problems according to the basic Isar scheme of
    1.26 -backward reasoning, the old tactic-style procedure may be mimicked as follows.
    1.27 -The general ML goal statement for derived rules looks like this:
    1.28 +are discharged again, resulting in the original rule statement.  The ``long
    1.29 +format'' of Isabelle/Isar goal statements admits to emulate this technique
    1.30 +closely.  The general ML goal statement for derived rules looks like this:
    1.31  \begin{ttbox}
    1.32   val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)";
    1.33   by \(tac@1\);
    1.34     \(\vdots\)
    1.35 + qed "\(a\)"
    1.36  \end{ttbox}
    1.37 -This form may be turned into a tactic-emulation script that is wrapped in an
    1.38 -Isar text to get access to the premises as local facts.
    1.39 +This form may be turned into a tactic-emulation script as follows:
    1.40  \begin{matharray}{l}
    1.41 -  \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
    1.42 -  \PROOF{}~- \\
    1.43 -  \quad \ASSUME{prem@1}{\phi@1}~\AND~\dots \\
    1.44 -  \quad \SHOW{}{\Var{thesis}} \\
    1.45 +  \LEMMA{a}{} \\
    1.46 +  \quad \ASSUMES{prem@1}{\texttt"\phi@1\texttt"}~\AND~\dots \\
    1.47 +  \quad \SHOWS{}{\texttt"{\psi}\texttt"} \\
    1.48    \qquad \APPLY{meth@1} \\
    1.49    \qquad\quad \vdots \\
    1.50    \qquad \DONE \\
    1.51 -  \QED{} \\
    1.52  \end{matharray}
    1.53 -Note that the above scheme repeats the text of premises $\phi@1$, \dots, while
    1.54 -the conclusion $\psi$ is referenced via the automatic text abbreviation
    1.55 -$\Var{thesis}$.  The assumption context may be invoked in a less verbose
    1.56 -manner as well, using ``$\CASE{rule_context}$'' instead of
    1.57 -``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above.  Then the list of \emph{all}
    1.58 -premises is bound to the name $rule_context$; Isar does not provide a way to
    1.59 -destruct lists into single items, though.
    1.60  
    1.61  \medskip In practice, actual rules are often rather direct consequences of
    1.62  corresponding atomic statements, typically stemming from the definition of a
    1.63 @@ -270,6 +256,21 @@
    1.64  conclusion; one may get this exact behavior by using
    1.65  ``$rule_format~(no_asm)$'' instead.
    1.66  
    1.67 +\medskip Actually ``$rule_format$'' is a bit unpleasant to work with, since
    1.68 +the final result statement is not shown in the text.  An alternative is to
    1.69 +state the resulting rule in the intended form in the first place, and have the
    1.70 +initial refinement step turn it into internal object-logic form using the
    1.71 +$atomize$ method indicated below.  The remaining script is unchanged.
    1.72 +
    1.73 +\begin{matharray}{l}
    1.74 +  \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
    1.75 +  \quad \APPLY{atomize~(full)} \\
    1.76 +  \quad \APPLY{meth@1} \\
    1.77 +  \qquad \vdots \\
    1.78 +  \quad \DONE \\
    1.79 +\end{matharray}
    1.80 +
    1.81 +
    1.82  \subsection{Tactics}\label{sec:conv-tac}
    1.83  
    1.84  Isar Proof methods closely resemble traditional tactics, when used in