
diff -r a90fc1e5fb19 -r abba35b98892 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue Aug 24 11:54:13 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Aug 24 15:38:18 1999 +0200
@@ -14,8 +14,8 @@
   erule^* & : & \isarmeth \\[0.5ex]
   fold & : & \isarmeth \\
   unfold & : & \isarmeth \\[0.5ex]
+  succeed & : & \isarmeth \\
   fail & : & \isarmeth \\
-  succeed & : & \isarmeth \\
 \end{matharray}
 
 \begin{rail}
@@ -25,12 +25,12 @@
 
 \begin{descr}
 \item [``$-$''] does nothing but insert the forward chaining facts as premises
-  into the goal.  Note that command $\PROOFNAME$ without any method given
-  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 (after inserting the
-  goal's facts).
+  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, 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.
@@ -41,24 +41,20 @@
   
   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 proof steps such as $\PROOFNAME$ and ``$\DDOT$'' (two dots).
-  
+  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).
 \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 script.  Actual elimination proofs are usually done with
-  $rule$ (single step) or $elim$ (multiple steps, see
+  porting of old scripts.  Actual elimination proofs are usually done with
+  $rule$ (single step, involving facts) or $elim$ (multiple steps, see
   \S\ref{sec:classical-basic}).
-  
-\item [$unfold~thms$ and $fold~thms$] expand and fold back again meta-level
-  definitions $thms$ throughout all goals; facts may not be given.
-
+\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
+  meta-level definitions throughout all goals; facts may not be involved.
+\item [$succeed$] yields a single (unchanged) result; it is the identify of
+  the ``\texttt{,}'' method combinator.
 \item [$fail$] yields an empty result sequence; it is the identify of the
   ``\texttt{|}'' method combinator.
-  
-\item [$succeed$] yields a singleton result, which is unchanged except for the
-  change from $prove$ mode back to $state$; it is the identify of the
-  ``\texttt{,}'' method combinator.
 \end{descr}
 
 
@@ -73,11 +69,11 @@
   OF & : & \isaratt \\
   RS & : & \isaratt \\
   COMP & : & \isaratt \\[0.5ex]
-  where & : & \isaratt \\
-  of & : & \isaratt \\[0.5ex]
+  of & : & \isaratt \\
+  where & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
   elimify & : & \isaratt \\
-  export & : & \isaratt \\
+  export^* & : & \isaratt \\
   transfer & : & \isaratt \\
 \end{matharray}
 
@@ -106,24 +102,23 @@
   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
   the reversed order).  $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 desired (see \texttt{RS} and \texttt{COMP} in
+  that is normally intended (see also \texttt{RS} and \texttt{COMP} in
   \cite[\S5]{isabelle-ref}).
   
-\item [$of~ts$ and $where~insts$] perform positional and named instantiation,
-  respectively.  The terms given in $of$ are substituted for any variables
-  occurring in a theorem from left to right; ``\texttt{_}'' (underscore)
-  indicates to skip a position.
+\item [$of~ts$ 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 (such as projection $conjunct@1$
-  into an elimination.
+\item [$elimify$] turns an destruction rule into an elimination.
   
 \item [$export$] lifts a local result out of the current proof context,
-  generalizing all fixed variables and discharging all assumptions.  Export is
-  usually done automatically behind the scenes.  This attribute is mainly for
-  experimentation.
+  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.
   
 \item [$transfer$] promotes a theorem to the current theory context, which has
   to enclose the former one.  Normally, this is done automatically when rules
@@ -175,24 +170,23 @@
 \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
-  \emph{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).
+  initialises $calculation$ by $facts$. 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).
   
 \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~\VVar{thesis}~\DOT$.
+  idiom is ``$\FINALLY~\SHOW{}{\VVar{thesis}}~\DOT$''.
   
-\item [Attribute $trans$] maintains the set of transitivity rules of the
-  theory or proof context, by adding or deleting the theorems provided as
-  arguments.  The default is adding of rules.
+\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 applications of
+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.
@@ -213,6 +207,7 @@
 theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
 tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
 the standard Isabelle documentation.
+%FIXME cite
 
 \begin{rail}
   'axclass' classdecl (axmdecl prop comment? +)
@@ -222,21 +217,23 @@
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{axclass}~$] defines an axiomatic type class as the
-  intersection of existing classes, with additional axioms holding.  Class
-  axioms may not contain more than one type variable.  The class axioms (with
-  implicit sort constraints added) are bound to the given names.  Furthermore
-  a class introduction rule is generated, which is employed by method
-  $expand_classes$ in support instantiation proofs of this class.
-
-\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
-  c@2$] setup up a goal stating the class relation or type arity.  The proof
-  would usually proceed by the $expand_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 [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
+  class as the intersection of existing classes, with additional axioms
+  holding.  Class axioms may not contain more than one type variable.  The
+  class axioms (with implicit sort constraints added) are bound to the given
+  names.  Furthermore a class introduction rule is generated, which is
+  employed by method $expand_classes$ in support instantiation proofs of this
+  class.
+  
+\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
+  (\vec s)c$] setup up a goal stating the class relation or type arity.  The
+  proof would usually proceed by the $expand_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 [Method $expand_classes$] iteratively expands the class introduction
   rules
+%FIXME intro classIs etc;
 \end{descr}
 
 See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
@@ -253,8 +250,11 @@
   asm_simp & : & \isarmeth \\
 \end{matharray}
 
+\railalias{asmsimp}{asm\_simp}
+\railterm{asmsimp}
+
 \begin{rail}
-  'simp' (simpmod * )
+  ('simp' | asmsimp) (simpmod * )
   ;
 
   simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
@@ -263,15 +263,16 @@
 
 \begin{descr}
 \item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
-  modifying the context as follows adding or deleting given rules.  The
+  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 manipulation of the context.
+  arbitrary context manipulation.
   
   Both of these methods are based on \texttt{asm_full_simp_tac}, see
-  \cite[\S10]{isabelle-ref}.
+  \cite[\S10]{isabelle-ref}; $simp$ removes any exisiting premises of the
+  goal, before inserting the goal facts; $asm_simp$ leaves the premises.
 \end{descr}
 
 \subsection{Modifying the context}
@@ -288,7 +289,7 @@
 
 \begin{descr}
 \item [Attribute $simp$] adds or deletes rules from the theory or proof
-  context.  The default is to add rules.
+  context (the default is to add).
 \end{descr}
 
 
@@ -303,13 +304,13 @@
 \end{matharray}
 
 These attributes provide forward rules for simplification, which should be
-used very rarely.  See the ML function of the same name in
+used only very rarely.  See the ML functions of the same name in
 \cite[\S10]{isabelle-ref} for more information.
 
 
 \section{The Classical Reasoner}
 
-\subsection{Basic step methods}\label{sec:classical-basic}
+\subsection{Basic methods}\label{sec:classical-basic}
 
 \indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
 \begin{matharray}{rcl}
@@ -329,14 +330,16 @@
   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.
+  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
   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 is
-  actually happening, thus it is appropriate as an initial proof method that
-  splits up certain connectives of the goal, before entering the sub-proof.
+  given ones may be applied.  The latter form admits better control of what
+  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.
@@ -370,11 +373,10 @@
 
 \begin{descr}
 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
-  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a applies a
+  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   user-supplied search bound (default 20).
 \item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
-  reasoner (see the corresponding tactics \texttt{fast_tac} etc.\ in
-  \cite[\S11]{isabelle-ref}).
+  reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
 \end{descr}
 
 Any of above methods support additional modifiers of the context of classical
@@ -403,7 +405,8 @@
   simplification and classical reasoning tactics.  See \texttt{force_tac} and
   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   modifier arguments correspond to those given in \S\ref{sec:simp} and
-  \S\ref{sec:classical-auto}.
+  \S\ref{sec:classical-auto}.  Note that the ones related to the Simplifier
+  are prefixed by \railtoken{simp} here.
 \end{descr}
 
 \subsection{Modifying the context}\label{sec:classical-mod}
@@ -422,13 +425,13 @@
 \end{rail}
 
 \begin{descr}
-\item [Attributes $intro$, $elim$, and $dest$] add introduction, elimination,
-  and 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).
-
-\item [Attribute $delrule$] deletes introduction or elimination rules from the
-  context.  Destruction rules would have to be turned into elimination rules
+\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).
+  
+\item [$delrule$] deletes introduction or elimination rules from the context.
+  Note that destruction rules would have to be turned into elimination rules
   first, e.g.\ by using the $elimify$ attribute.
 \end{descr}
 




