--- a/doc-src/IsarRef/generic.tex Thu Oct 21 17:42:42 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Thu Oct 21 18:04:07 1999 +0200
@@ -29,29 +29,30 @@
plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
$\PROOFNAME$ alone.
\item [$assumption$] solves some goal by assumption. Any facts given are
- guaranteed to participate in the refinement.
+ guaranteed to participate in the refinement. Note that ``$\DOT$'' (dot)
+ abbreviates $\BY{assumption}$.
\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
- becomes an \emph{elimination}.
+ becomes a (generalized) \emph{elimination}.
Note that the classical reasoner introduces another version of $rule$ that
is able to pick appropriate rules automatically, whenever explicit $thms$
are omitted (see \S\ref{sec:classical-basic}); that method is the default
- one for initial proof steps, such as $\PROOFNAME$ and ``$\DDOT$'' (two
- dots).
+ for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates
+ $\BY{default}$.
\item [$erule~thms$] is similar to $rule$, but applies rules by
elim-resolution. This is an improper method, mainly for experimentation and
porting of old scripts. Actual elimination proofs are usually done with
- $rule$ (single step, involving facts) or $elim$ (multiple steps, see
+ $rule$ (single step, involving facts) or $elim$ (repeated steps, see
\S\ref{sec:classical-basic}).
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
meta-level definitions throughout all goals; any facts provided are
\emph{ignored}.
\item [$succeed$] yields a single (unchanged) result; it is the identify of
- the ``\texttt{,}'' method combinator.
+ the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
\item [$fail$] yields an empty result sequence; it is the identify of the
- ``\texttt{|}'' method combinator.
+ ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
\end{descr}
@@ -91,9 +92,9 @@
\end{rail}
\begin{descr}
-\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
+\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
respectively. Tags may be any list of strings that serve as comment for
- some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the
+ some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
result).
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
@@ -102,8 +103,7 @@
$RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
that does not include the automatic lifting process that is normally
- intended (see also \texttt{RS} and \texttt{COMP} in
- \cite[\S5]{isabelle-ref}).
+ intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
instantiation, respectively. The terms given in $of$ are substituted for
@@ -113,7 +113,8 @@
\item [$standard$] puts a theorem into the standard form of object-rules, just
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
-\item [$elimify$] turns an destruction rule into an elimination.
+\item [$elimify$] turns an destruction rule into an elimination, just as the
+ ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
\item [$export$] lifts a local result out of the current proof context,
generalizing all fixed variables and discharging all assumptions. Note that
@@ -139,12 +140,12 @@
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 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
-after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
-some finished $\HAVENAME$ or $\SHOWNAME$.
+results obtained by transitivity composed with the current result. Command
+$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
+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.
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
application with calculational proofs. It automatically refers to the
@@ -179,17 +180,19 @@
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
$\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{}{\Var{thesis}}~\DOT$''.
+ $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Typical proof
+ idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
+ ``$\FINALLY~\HAVE{}{\phi}~\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).
\end{descr}
-See theory \texttt{HOL/Isar_examples/Group} for a simple application of
-calculations for basic equational reasoning.
-\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
-calculational steps in combination with natural deduction.
+%FIXME
+%See theory \texttt{HOL/Isar_examples/Group} for a simple application of
+%calculations for basic equational reasoning.
+%\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
+%calculational steps in combination with natural deduction.
\section{Axiomatic Type Classes}\label{sec:axclass}
@@ -231,7 +234,7 @@
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 [$intro_classes$] iteratively expands the class introduction rules of
+\item [$intro_classes$] repeatedly expands the class introduction rules of
this theory.
\end{descr}
@@ -243,17 +246,13 @@
\subsection{Simplification methods}\label{sec:simp}
-\indexisarmeth{simp}\indexisarmeth{asm-simp}
+\indexisarmeth{simp}
\begin{matharray}{rcl}
simp & : & \isarmeth \\
- asm_simp & : & \isarmeth \\
\end{matharray}
-\railalias{asmsimp}{asm\_simp}
-\railterm{asmsimp}
-
\begin{rail}
- ('simp' | asmsimp) (simpmod * )
+ 'simp' (simpmod * )
;
simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
@@ -261,15 +260,20 @@
\end{rail}
\begin{descr}
-\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;
+\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
+ adding or deleting rules as specified. 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 premises of the goal, before
+ The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
+ \cite[\S10]{isabelle-ref}), but is much better behaved in practice. Only
+ the local premises of the actual goal are involved by default. Additional
+ facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
+ The full context of assumptions is
+
+; $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