--- a/doc-src/IsarRef/generic.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Sat Sep 04 20:57:32 1999 +0200
@@ -28,8 +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. The facts (if any) are
- guaranteed to participate.
+\item [$assumption$] solves some goal by assumption. Any facts given are
+ guaranteed to participate in the refinement.
\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
@@ -104,7 +104,7 @@
intended (see also \texttt{RS} and \texttt{COMP} in
\cite[\S5]{isabelle-ref}).
-\item [$of~ts$ and $where~\vec x = \vec t$] perform positional and named
+\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
instantiation, respectively. The terms given in $of$ are substituted for
any schematic variables occurring in a theorem from left to right;
``\texttt{_}'' (underscore) indicates to skip a position.
@@ -179,7 +179,7 @@
$\ALSO$, and concludes the current calculational thread. The final result
is exhibited as fact for forward chaining towards the next goal. Basically,
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof
- idiom is ``$\FINALLY~\SHOW{}{\VVar{thesis}}~\DOT$''.
+ idiom is ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''.
\item [$trans$] maintains the set of transitivity rules of the theory or proof
context, by adding or deleting theorems (the default is to add).
@@ -230,8 +230,8 @@
establish the characteristic theorems of the type classes involved. After
finishing the proof the theory will be augmented by a type signature
declaration corresponding to the resulting theorem.
-\item [Method $intro_classes$] iteratively expands the class introduction
- rules
+\item [$intro_classes$] iteratively expands the class introduction rules of
+ this theory.
\end{descr}
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
@@ -260,17 +260,20 @@
\end{rail}
\begin{descr}
-\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
- modifying the context by adding or deleting given rules. The
- \railtoken{only} modifier first removes all other rewrite rules and
- congruences, and then is like \railtoken{add}. In contrast,
- \railtoken{other} ignores its arguments; nevertheless there may be
- side-effects on the context via attributes. This provides a back door for
- arbitrary context manipulation.
+\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying
+ the context by adding or deleting given rules. The \railtoken{only}
+ modifier first removes all other rewrite rules and congruences, and then is
+ like \railtoken{add}. In contrast, \railtoken{other} ignores its arguments;
+ nevertheless there may be side-effects on the context via attributes. This
+ provides a back door for arbitrary context manipulation.
Both of these methods are based on \texttt{asm_full_simp_tac}, see
- \cite[\S10]{isabelle-ref}; $simp$ removes any exisiting premises of the
- goal, before inserting the goal facts; $asm_simp$ leaves the premises.
+ \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before
+ inserting the goal facts; $asm_simp$ leaves the premises. Thus $asm_simp$
+ may refer to premises that are not explicitly spelled out, potentially
+ obscuring the reasoning. The plain $simp$ method is more faithful in the
+ sense that, apart from the rewrite rules of the current context, \emph{at
+ most} the explicitly provided facts may participate in the simplification.
\end{descr}
\subsection{Modifying the context}
@@ -286,8 +289,8 @@
\end{rail}
\begin{descr}
-\item [Attribute $simp$] adds or deletes rules from the theory or proof
- context (the default is to add).
+\item [$simp$] adds or deletes rules from the theory or proof context (the
+ default is to add).
\end{descr}
@@ -325,14 +328,14 @@
\end{rail}
\begin{descr}
-\item [Method $rule$] as offered by the classical reasoner is a refinement
- over the primitive one (see \S\ref{sec:pure-meth}). In the case that no
- rules are provided as arguments, it automatically determines elimination and
+\item [$rule$] as offered by the classical reasoner is a refinement over the
+ primitive one (see \S\ref{sec:pure-meth}). In the case that no rules are
+ provided as arguments, it automatically determines elimination and
introduction rules from the context (see also \S\ref{sec:classical-mod}).
In that form it is the default method for basic proof steps, such as
$\PROOFNAME$ and ``$\DDOT$'' (two dots).
-\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or
+\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
elim-resolution, after having inserted the facts. Omitting the arguments
refers to any suitable rules from the context, otherwise only the explicitly
given ones may be applied. The latter form admits better control of what
@@ -340,9 +343,9 @@
$\PROOFNAME$ that splits up certain connectives of the goal, before entering
the sub-proof.
-\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.
+\item [$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}
@@ -430,7 +433,7 @@
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
respectively. By default, rules are considered as \emph{safe}, while a
single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\
- not applied in the search-oriented automatic methods).
+ not applied in the search-oriented automatic methods, but only $rule$).
\item [$iff$] declares equations both as rewrite rules for the simplifier and
classical reasoning rules.