# HG changeset patch
# User wenzelm
# Date 935414847 -7200
# Node ID b4dcc32310fbc7e9d826b8cadaa5c6be5270f0f7
# Parent  e89fd7d0a6249a4ffabb4ee22a60899ac1ee3eab
tuned;

diff -r e89fd7d0a624 -r b4dcc32310fb doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Aug 23 15:27:27 1999 +0200
@@ -7,15 +7,15 @@
 \indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
 \indexisarmeth{rule}\indexisarmeth{erule}
 \begin{matharray}{rcl}
-  fail & : & \isarmeth \\
-  succeed & : & \isarmeth \\
   - & : & \isarmeth \\
   assumption & : & \isarmeth \\
-  finish & : & \isarmeth \\
+  finish & : & \isarmeth \\[0.5ex]
+  rule & : & \isarmeth \\
+  erule^* & : & \isarmeth \\[0.5ex]
   fold & : & \isarmeth \\
-  unfold & : & \isarmeth \\
-  rule & : & \isarmeth \\
-  erule^* & : & \isarmeth \\
+  unfold & : & \isarmeth \\[0.5ex]
+  fail & : & \isarmeth \\
+  succeed & : & \isarmeth \\
 \end{matharray}
 
 \begin{rail}
@@ -24,14 +24,42 @@
 \end{rail}
 
 \begin{descr}
-\item [$ $]
-\end{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).
+\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 [$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}.
+  
+  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).
+  
+\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
+  \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.
 
-FIXME
-
-%FIXME sort
-%FIXME thmref (single)
-%FIXME var vs. term
+\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}
 
 
 \section{Miscellaneous attributes}
@@ -41,46 +69,68 @@
 \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
 \begin{matharray}{rcl}
   tag & : & \isaratt \\
-  untag & : & \isaratt \\
-  COMP & : & \isaratt \\
+  untag & : & \isaratt \\[0.5ex]
+  OF & : & \isaratt \\
   RS & : & \isaratt \\
-  OF & : & \isaratt \\
+  COMP & : & \isaratt \\[0.5ex]
   where & : & \isaratt \\
-  of & : & \isaratt \\
+  of & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
   elimify & : & \isaratt \\
+  export & : & \isaratt \\
   transfer & : & \isaratt \\
-  export & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
   ('tag' | 'untag') (nameref+)
   ;
-\end{rail}
-
-\begin{rail}
-  ('COMP' | 'RS') nat? thmref
-  ;
   'OF' thmrefs
   ;
-\end{rail}
-
-\begin{rail}
-  'where' (name '=' term * 'and')
+  ('RS' | 'COMP') nat? thmref
   ;
   'of' (inst * ) ('concl' ':' (inst * ))?
   ;
+  'where' (name '=' term * 'and')
+  ;
 
   inst: underscore | term
   ;
 \end{rail}
 
 \begin{descr}
-\item [$ $]
+\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to 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
+  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).  $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
+  \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 [$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 [$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.
+  
+\item [$transfer$] promotes a theorem to the current theory context, which has
+  to enclose the former one.  Normally, this is done automatically when rules
+  are joined by inference.
+
 \end{descr}
 
-FIXME
-
 
 \section{Calculational proof}\label{sec:calculation}
 
@@ -172,7 +222,13 @@
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{axclass}~$] FIXME
+\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
@@ -189,13 +245,12 @@
 
 \section{The Simplifier}
 
-\subsection{Simplification methods}
+\subsection{Simplification methods}\label{sec:simp}
 
-\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
+\indexisarmeth{simp}\indexisarmeth{asm_simp}
 \begin{matharray}{rcl}
   simp & : & \isarmeth \\
   asm_simp & : & \isarmeth \\
-  simp & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
@@ -206,7 +261,35 @@
   ;
 \end{rail}
 
-FIXME
+\begin{descr}
+\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
+  modifying the context as follows 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.
+  
+  Both of these methods are based on \texttt{asm_full_simp_tac}, see
+  \cite[\S10]{isabelle-ref}.
+\end{descr}
+
+\subsection{Modifying the context}
+
+\indexisaratt{simp}
+\begin{matharray}{rcl}
+  simp & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+  'simp' (() | 'add' | 'del')
+  ;
+\end{rail}
+
+\begin{descr}
+\item [Attribute $simp$] adds or deletes rules from the theory or proof
+  context.  The default is to add rules.
+\end{descr}
 
 
 \subsection{Forward simplification}
@@ -219,33 +302,135 @@
   asm_full_simplify & : & \isaratt \\
 \end{matharray}
 
-FIXME
+These attributes provide forward rules for simplification, which should be
+used very rarely.  See the ML function of the same name in
+\cite[\S10]{isabelle-ref} for more information.
 
 
 \section{The Classical Reasoner}
 
-\subsection{Single step methods}
+\subsection{Basic step methods}\label{sec:classical-basic}
+
+\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
+\begin{matharray}{rcl}
+  rule & : & \isarmeth \\
+  intro & : & \isarmeth \\
+  elim & : & \isarmeth \\
+  contradiction & : & \isarmeth \\
+\end{matharray}
+
+\begin{rail}
+  ('rule' | 'intro' | 'elim') thmrefs
+  ;
+\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
+  introduction rules from the context (see also \S\ref{sec:classical-mod}).
+  In that form it is the default method for basic proof steps.
+  
+\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.
+
+\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
+  $\neg A$ have to be present in the assumptions.
+\end{descr}
+
+
+\subsection{Automatic methods}\label{sec:classical-auto}
 
-\subsection{Automatic methods}
+\indexisarmeth{blast}
+\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}
+\begin{matharray}{rcl}
+ blast & : & \isarmeth \\
+ fast & : & \isarmeth \\
+ best & : & \isarmeth \\
+ slow & : & \isarmeth \\
+ slow_best & : & \isarmeth \\
+\end{matharray}
+
+\railalias{slowbest}{slow\_best}
+\railterm{slowbest}
+
+\begin{rail}
+  'blast' nat? (clamod * )
+  ;
+  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
+  ;
+
+  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
+  ;
+\end{rail}
+
+\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
+  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}).
+\end{descr}
+
+Any of above methods support additional modifiers of the context of classical
+rules.  There semantics is analogous to the attributes given in
+\S\ref{sec:classical-mod}.
+
 
 \subsection{Combined automatic methods}
 
-\subsection{Modifying the context}
+\indexisarmeth{auto}\indexisarmeth{force}
+\begin{matharray}{rcl}
+  force & : & \isarmeth \\
+  auto & : & \isarmeth \\
+\end{matharray}
+
+\begin{rail}
+  ('force' | 'auto') (clasimpmod * )
+  ;
 
+  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
+    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
+\end{rail}
 
+\begin{descr}
+\item [$force$ and $auto$] provide access to Isabelle's combined
+  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}.
+\end{descr}
+
+\subsection{Modifying the context}\label{sec:classical-mod}
 
-%\indexisarcmd{}
-%\begin{matharray}{rcl}
-%  \isarcmd{} & : & \isartrans{}{} \\
-%\end{matharray}
+\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}
+\begin{matharray}{rcl}
+  intro & : & \isaratt \\
+  elim & : & \isaratt \\
+  dest & : & \isaratt \\
+  delrule & : & \isaratt \\
+\end{matharray}
 
-%\begin{rail}
-  
-%\end{rail}
+\begin{rail}
+  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
+  ;
+\end{rail}
 
-%\begin{descr}
-%\item [$ $]
-%\end{descr}
+\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
+  first, e.g.\ by using the $elimify$ attribute.
+\end{descr}
 
 
 %%% Local Variables: 
diff -r e89fd7d0a624 -r b4dcc32310fb doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Mon Aug 23 15:27:27 1999 +0200
@@ -659,8 +659,8 @@
   Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
   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{-}$, where
+\item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$.
+\item [``$\DOT$''] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
   method ``$-$'' does nothing except inserting any facts into the proof state.
 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
   \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
diff -r e89fd7d0a624 -r b4dcc32310fb doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Mon Aug 23 15:27:27 1999 +0200
@@ -134,7 +134,7 @@
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
 \indexouternonterm{classdecl}
 \begin{rail}
-  classdecl: name ('<' (nameref ',' +))?
+  classdecl: name ('<' (nameref + ','))?
   ;
   sort: nameref | lbrace (nameref * ',') rbrace
   ;
diff -r e89fd7d0a624 -r b4dcc32310fb doc-src/iman.sty
--- a/doc-src/iman.sty	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/iman.sty	Mon Aug 23 15:27:27 1999 +0200
@@ -36,8 +36,6 @@
 
 \newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
 \newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
-\newcommand\attdx[1]{$#1$\index{#1@$#1$ attribute}}
-\newcommand\methdx[1]{$#1$\index{#1@$#1$ proof method}}
 
 %for cross-references: 2nd argument (page number) is ignored
 \newcommand\see[2]{{\it see \/}{#1}}
diff -r e89fd7d0a624 -r b4dcc32310fb doc-src/isar.sty
--- a/doc-src/isar.sty	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/isar.sty	Mon Aug 23 15:27:27 1999 +0200
@@ -57,7 +57,7 @@
 \newcommand{\DEFS}{\isarkeyword{defs}}
 \newcommand{\TEXT}{\isarkeyword{text}}
 \newcommand{\TXT}{\isarkeyword{txt}}
-\newcommand{\NOTE}[2]{\NOTENAME\ifthenelse{\equal{}{#1}}{}{~#1=}#2}
+\newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
 \newcommand{\FROM}[1]{\FROMNAME~#1}
 \newcommand{\WITH}[1]{\WITHNAME~#1}
 \newcommand{\FIX}[1]{\FIXNAME~#1}