author | wenzelm |

Mon Mar 04 19:07:22 2002 +0100 (2002-03-04) | |

changeset 13013 | 4db07fc3d96f |

parent 13012 | f8bfc61ee1b5 |

child 13014 | 3c1c493e6d93 |

improved ``deriving rules'';

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