--- a/doc-src/IsarRef/generic.tex Thu Mar 30 15:11:48 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Thu Mar 30 15:12:20 2000 +0200
@@ -47,10 +47,14 @@
\section{Calculational proof}\label{sec:calculation}
-\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
+\indexisarcmd{also}\indexisarcmd{finally}
+\indexisarcmd{moreover}\indexisarcmd{ultimately}
+\indexisaratt{trans}
\begin{matharray}{rcl}
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
+ \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
trans & : & \isaratt \\
\end{matharray}
@@ -62,12 +66,14 @@
final $calculation$ by forward chaining towards the next goal statement. Both
commands require valid current facts, i.e.\ may occur only after commands that
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
-$\HAVENAME$, $\SHOWNAME$ etc.
+$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are
+similar to $\ALSO$ and $\FINALLY$, but only collect further results in
+$calculation$ without applying any rules yet.
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
-application with calculational proofs. It automatically refers to the
-argument\footnote{The argument of a curried infix expression is its right-hand
- side.} of the preceding statement.
+application with calculational proofs. It refers to the argument\footnote{The
+ argument of a curried infix expression is its right-hand side.} of the
+preceding statement.
Isabelle/Isar calculations are implicitly subject to block structure in the
sense that new threads of calculational reasoning are commenced for any new
@@ -75,9 +81,24 @@
being able to nest calculations, there is no separate \emph{begin-calculation}
command required.
+\medskip
+
+The Isar calculation proof commands may be defined as
+follows:\footnote{Internal bookkeeping such as proper handling of
+ block-structure has been suppressed.}
+\begin{matharray}{rcl}
+ \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
+ \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\
+ \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
+ \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
+ \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
+\end{matharray}
+
\begin{rail}
('also' | 'finally') transrules? comment?
;
+ ('moreover' | 'ultimately') comment?
+ ;
'trans' (() | 'add' | 'del')
;
@@ -102,6 +123,9 @@
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
calculational proofs.
+\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
+ but collect results only, without applying rules.
+
\item [$trans$] declares theorems as transitivity rules.
\end{descr}
--- a/doc-src/IsarRef/refcard.tex Thu Mar 30 15:11:48 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex Thu Mar 30 15:12:20 2000 +0200
@@ -58,10 +58,16 @@
\ALSO@0 & \approx & \NOTE{calculation}{this} \\
\ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
\FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]
- \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi}~~\text{(permissive assumption)} \\
- \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t}~~\text{(definitional assumption)} \\
- \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi}~~\text{(generalized existence)} \\
- \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi}~~\text{(named context)} \\[0.5ex]
+ \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
+ \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
+ \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
+% & & \text{(permissive assumption)} \\
+ \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
+% & & \text{(definitional assumption)} \\
+ \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
+% & & \text{(generalized existence)} \\
+ \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
+% & & \text{(named context)} \\[0.5ex]
\SORRY & \approx & \BY{cheating} \\
\end{matharray}