author wenzelm Fri, 03 Sep 1999 16:11:53 +0200 changeset 7458 bb282845ca77 parent 7457 e67eed4cd224 child 7459 173efad74891
updated;
 doc-src/IsarRef/generic.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/pure.tex file | annotate | diff | comparison | revisions
--- 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.