--- a/doc-src/IsarRef/generic.tex Fri Sep 03 16:11:03 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Sep 03 16:11:53 1999 +0200
@@ -4,12 +4,11 @@
\section{Basic proof methods}\label{sec:pure-meth}
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
-\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
+\indexisarmeth{fold}\indexisarmeth{unfold}
\indexisarmeth{rule}\indexisarmeth{erule}
\begin{matharray}{rcl}
- & : & \isarmeth \\
assumption & : & \isarmeth \\
- finish & : & \isarmeth \\[0.5ex]
rule & : & \isarmeth \\
erule^* & : & \isarmeth \\[0.5ex]
fold & : & \isarmeth \\
@@ -29,11 +28,8 @@
performs a single reduction step using the $rule$ method (see below); thus a
plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
$\PROOFNAME$ alone.
-\item [$assumption$] solves some goal by assumption, after inserting the
- goal's facts.
-\item [$finish$] solves all remaining goals by assumption; this is the default
- terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be
- spelled out explicitly.
+\item [$assumption$] solves some goal by assumption. The facts (if any) are
+ guaranteed to participate.
\item [$rule~thms$] applies some rule given as argument in backward manner;
facts are used to reduce the rule before applying it to the goal. Thus
$rule$ without facts is plain \emph{introduction}, while with facts it
@@ -142,7 +138,7 @@
Calculational proof is forward reasoning with implicit application of
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
-results obtained by transitivity obtained together with the current facts.
+results obtained by transitivity obtained together with the current result.
Command $\ALSO$ updates $calculation$ from the most recent result, while
$\FINALLY$ exhibits the final result by forward chaining towards the next goal
statement. Both commands require valid current facts, i.e.\ may occur only
@@ -173,11 +169,11 @@
\begin{descr}
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
follows. The first occurrence of $\ALSO$ in some calculational thread
- initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the same
+ initialises $calculation$ by $this$. Any subsequent $\ALSO$ on the same
level of block-structure updates $calculation$ by some transitivity rule
- applied to $calculation$ and $facts$ (in that order). Transitivity rules
- are picked from the current context plus those given as $thms$ (the latter
- have precedence).
+ applied to $calculation$ and $this$ (in that order). Transitivity rules are
+ picked from the current context plus those given as $thms$ (the latter have
+ precedence).
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
$\ALSO$, and concludes the current calculational thread. The final result
@@ -343,9 +339,10 @@
actually happens, thus it is very appropriate as an initial method for
$\PROOFNAME$ that splits up certain connectives of the goal, before entering
the sub-proof.
-
-\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
- $\neg A$ have to be present in the assumptions.
+
+\item [Method $contradiction$] solves some goal by contradiction, deriving any
+ result from both $\neg A$ and $A$. Facts, which are guaranteed to
+ participate, may appear in either order.
\end{descr}
--- a/doc-src/IsarRef/pure.tex Fri Sep 03 16:11:03 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Fri Sep 03 16:11:53 1999 +0200
@@ -410,8 +410,8 @@
\item [$proof(state)$] is like an internal theory mode: the context may be
augmented by \emph{stating} additional assumptions, intermediate result etc.
\item [$proof(chain)$] is an intermediate mode between $proof(state)$ and
- $proof(prove)$: existing facts have been just picked up in order to use them
- when refining the goal claimed next.
+ $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
+ picked up in order to use them when refining the goal claimed next.
\end{descr}
@@ -478,7 +478,7 @@
var: name ('::' type)?
;
- vars: name+ ('::' type)?
+ vars: (name+) ('::' type)?
;
assm: thmdecl? (prop proppat? +)
;
@@ -521,7 +521,7 @@
Any fact will usually be involved in further proofs, either as explicit
arguments of proof methods or when forward chaining towards the next goal via
$\THEN$ (and variants). Note that the special theorem name
-$facts$.\indexisarthm{facts} refers to the most recently established facts.
+$this$.\indexisarthm{this} refers to the most recently established facts.
\begin{rail}
'note' thmdef? thmrefs comment?
;
@@ -541,7 +541,7 @@
\S\ref{sec:proof-steps}). For example, method $rule$ (see
\S\ref{sec:pure-meth}) would do an elimination rather than an introduction.
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
- equivalent to $\FROM{facts}$.
+ equivalent to $\FROM{this}$.
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
chaining is from earlier facts together with the current ones.
\end{descr}
@@ -549,9 +549,9 @@
Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
multiple facts to be given in proper order, corresponding to a prefix of the
premises of the rule involved. Note that positions may be easily skipped
-using a form like $\FROM{_~a~b}$, for example. This involves the rule
-$PROP~\psi \Imp PROP~\psi$, which is bound in Isabelle/Pure as ``_''
-(underscore).\indexisarthm{_@\texttt{_}}
+using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves
+the rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure as
+``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
\subsection{Goal statements}
@@ -593,8 +593,10 @@
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
pending goal with the result \emph{exported} into the corresponding context.
\item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a
- local goal to be proven by forward chaining the current facts.
-\item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$.
+ local goal to be proven by forward chaining the current facts. Note that
+ $\HENCENAME$ is equivalent to $\FROM{this}~\HAVENAME$.
+\item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. Note that
+ $\THUSNAME$ is equivalent to $\FROM{this}~\SHOWNAME$.
\end{descr}
@@ -639,8 +641,9 @@
Unless given explicitly by the user, the default initial method is
``$default$'', which is usually set up to apply a single standard elimination
-or introduction rule according to the topmost symbol involved. The default
-terminal method is ``$finish$''; it solves all goals by assumption.
+or introduction rule according to the topmost symbol involved. There is no
+default terminal method; in any case the final step is to solve all remaining
+goals by assumption.
\begin{rail}
'proof' interest? meth? comment?
@@ -673,7 +676,8 @@
expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
sufficient to see what is going wrong.
\item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$.
-\item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates $\BY{-}$.
+\item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates
+ $\BY{assumption}$.
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
\texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
the goal without further ado. Of course, the result is a fake theorem only,
@@ -734,7 +738,7 @@
higher-order matching is applied to bind extra-logical text
variables\index{text variables}, which may be either of the form $\VVar{x}$
(token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless
-dummies ``\verb,_,'' (underscore).\index{dummy variables} Note that in the
+dummies ``\texttt{_}'' (underscore).\index{dummy variables} Note that in the
$\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$
patterns are in postfix position.