doc-src/IsarRef/generic.tex

   into the goal.  Note that command $\PROOFNAME$ without any method actually
   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.  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}
 
 
 \section{Miscellaneous attributes}
 

   inst: underscore | term
   ;
 \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
   the reversed order).  Note that premises may be skipped by including $\_$
   (underscore) as argument.
   
   $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
   any schematic variables occurring in a theorem from left to right;
   ``\texttt{_}'' (underscore) indicates to skip a position.
  
 \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
   (partial) export is usually done automatically behind the scenes.  This
   attribute is mainly for experimentation.

 \end{matharray}
 
 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
 argument\footnote{The argument of a curried infix expression is its right-hand
   side.} of the preceding statement.

   precedence).
   
 \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}
 
 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}

   (\vec s)c$] setup up a goal stating the class relation or type arity.  The
   proof would usually proceed by the $intro_classes$ method, and then
   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}
 
 See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
 axiomatic type classes, including instantiation proofs.

 
 \section{The Simplifier}
 
 \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 * )
+\end{matharray}
+
+\begin{rail}
+  'simp' (simpmod * )
   ;
 
   simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
   ;
 \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
   sense that, apart from the rewrite rules of the current context, \emph{at
     most} the explicitly provided facts may participate in the simplification.