doc-src/IsarRef/generic.tex
changeset 7987 d9aef93c0e32
parent 7981 5120a2a15d06
child 7990 0a604b2fc2b1
     1.1 --- a/doc-src/IsarRef/generic.tex	Sat Oct 30 20:41:30 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Oct 31 15:20:35 1999 +0100
     1.3 @@ -37,9 +37,9 @@
     1.4    becomes a (generalized) \emph{elimination}.
     1.5    
     1.6    Note that the classical reasoner introduces another version of $rule$ that
     1.7 -  is able to pick appropriate rules automatically, whenever explicit $thms$
     1.8 -  are omitted (see \S\ref{sec:classical-basic}); that method is the default
     1.9 -  for $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
    1.10 +  is able to pick appropriate rules automatically, whenever $thms$ are omitted
    1.11 +  (see \S\ref{sec:classical-basic}); that method is the default for
    1.12 +  $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
    1.13    $\BY{default}$.
    1.14  \item [$erule~thms$] is similar to $rule$, but applies rules by
    1.15    elim-resolution.  This is an improper method, mainly for experimentation and
    1.16 @@ -47,11 +47,11 @@
    1.17    $rule$ (single step, involving facts) or $elim$ (repeated steps, see
    1.18    \S\ref{sec:classical-basic}).
    1.19  \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
    1.20 -  meta-level definitions throughout all goals; any facts provided are
    1.21 -  \emph{ignored}.
    1.22 -\item [$succeed$] yields a single (unchanged) result; it is the identify of
    1.23 +  meta-level definitions throughout all goals; any facts provided are inserted
    1.24 +  into the goal and subject to rewriting as well.
    1.25 +\item [$succeed$] yields a single (unchanged) result; it is the identity of
    1.26    the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.27 -\item [$fail$] yields an empty result sequence; it is the identify of the
    1.28 +\item [$fail$] yields an empty result sequence; it is the identity of the
    1.29    ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.30  \end{descr}
    1.31  
    1.32 @@ -98,12 +98,12 @@
    1.33    result).
    1.34  \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
    1.35    $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
    1.36 -  the reversed order).  Note that premises may be skipped by including $\_$
    1.37 -  (underscore) as argument.
    1.38 +  the reversed order).  Note that premises may be skipped by including
    1.39 +  ``$\_$'' (underscore) as argument.
    1.40    
    1.41    $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
    1.42 -  that does not include the automatic lifting process that is normally
    1.43 -  intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
    1.44 +  that skips the automatic lifting process that is normally intended (cf.\ 
    1.45 +  \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
    1.46    
    1.47  \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
    1.48    instantiation, respectively.  The terms given in $of$ are substituted for
    1.49 @@ -180,9 +180,10 @@
    1.50  \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
    1.51    $\ALSO$, and concludes the current calculational thread.  The final result
    1.52    is exhibited as fact for forward chaining towards the next goal. Basically,
    1.53 -  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Typical proof
    1.54 -  idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
    1.55 -  ``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
    1.56 +  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
    1.57 +  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
    1.58 +  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
    1.59 +  calculational proofs.
    1.60    
    1.61  \item [$trans$] maintains the set of transitivity rules of the theory or proof
    1.62    context, by adding or deleting theorems (the default is to add).
    1.63 @@ -204,12 +205,12 @@
    1.64    intro_classes & : & \isarmeth \\
    1.65  \end{matharray}
    1.66  
    1.67 -Axiomatic type classes are provided by Isabelle/Pure as a purely
    1.68 -\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
    1.69 -any object logic may make use of this light-weight mechanism for abstract
    1.70 -theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
    1.71 -tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
    1.72 -the standard Isabelle documentation.
    1.73 +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
    1.74 +interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
    1.75 +may make use of this light-weight mechanism of abstract theories.  See
    1.76 +\cite{Wenzel:1997:TPHOL} for more information.  There is also a tutorial on
    1.77 +\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard
    1.78 +Isabelle documentation.
    1.79  %FIXME cite
    1.80  
    1.81  \begin{rail}
    1.82 @@ -225,21 +226,22 @@
    1.83    holding.  Class axioms may not contain more than one type variable.  The
    1.84    class axioms (with implicit sort constraints added) are bound to the given
    1.85    names.  Furthermore a class introduction rule is generated, which is
    1.86 -  employed by method $intro_classes$ in support instantiation proofs of this
    1.87 +  employed by method $intro_classes$ to support instantiation proofs of this
    1.88    class.
    1.89    
    1.90  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
    1.91    (\vec s)c$] setup up a goal stating the class relation or type arity.  The
    1.92 -  proof would usually proceed by the $intro_classes$ method, and then
    1.93 -  establish the characteristic theorems of the type classes involved.  After
    1.94 -  finishing the proof the theory will be augmented by a type signature
    1.95 -  declaration corresponding to the resulting theorem.
    1.96 -\item [$intro_classes$] repeatedly expands the class introduction rules of
    1.97 +  proof would usually proceed by $intro_classes$, and then establish the
    1.98 +  characteristic theorems of the type classes involved.  After finishing the
    1.99 +  proof, the theory will be augmented by a type signature declaration
   1.100 +  corresponding to the resulting theorem.
   1.101 +\item [$intro_classes$] repeatedly expands all class introduction rules of
   1.102    this theory.
   1.103  \end{descr}
   1.104  
   1.105 -See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
   1.106 -axiomatic type classes, including instantiation proofs.
   1.107 +%FIXME
   1.108 +%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
   1.109 +%axiomatic type classes, including instantiation proofs.
   1.110  
   1.111  
   1.112  \section{The Simplifier}
   1.113 @@ -345,7 +347,7 @@
   1.114    given ones may be applied.  The latter form admits better control of what
   1.115    actually happens, thus it is very appropriate as an initial method for
   1.116    $\PROOFNAME$ that splits up certain connectives of the goal, before entering
   1.117 -  the actual proof.
   1.118 +  the actual sub-proof.
   1.119    
   1.120  \item [$contradiction$] solves some goal by contradiction, deriving any result
   1.121    from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   1.122 @@ -388,7 +390,10 @@
   1.123  
   1.124  Any of above methods support additional modifiers of the context of classical
   1.125  rules.  There semantics is analogous to the attributes given in
   1.126 -\S\ref{sec:classical-mod}.
   1.127 +\S\ref{sec:classical-mod}.  Facts provided by forward chaining are inserted
   1.128 +into the goal before doing the search.  The ``!''~argument causes the full
   1.129 +context of assumptions to be included as well.\footnote{This is slightly less
   1.130 +  hazardous than for the Simplifier (see \S\ref{sec:simp}).}
   1.131  
   1.132  
   1.133  \subsection{Combined automated methods}
   1.134 @@ -403,7 +408,7 @@
   1.135    ('force' | 'auto') ('!' ?) (clasimpmod * )
   1.136    ;
   1.137  
   1.138 -  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
   1.139 +  clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
   1.140      (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
   1.141  \end{rail}
   1.142  
   1.143 @@ -414,8 +419,13 @@
   1.144    modifier arguments correspond to those given in \S\ref{sec:simp} and
   1.145    \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.146    Simplifier are prefixed by \railtoken{simp} here.
   1.147 +  
   1.148 +  Facts provided by forward chaining are inserted into the goal before doing
   1.149 +  the search.  The ``!''~argument causes the full context of assumptions to be
   1.150 +  included as well.
   1.151  \end{descr}
   1.152  
   1.153 +
   1.154  \subsection{Modifying the context}\label{sec:classical-mod}
   1.155  
   1.156  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}