tuned;
authorwenzelm
Thu Oct 21 18:45:55 1999 +0200 (1999-10-21)
changeset 7905c5f735f7428c
parent 7904 2b551893583e
child 7906 0576dad973b1
tuned;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Oct 21 18:45:31 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Oct 21 18:45:55 1999 +0200
     1.3 @@ -171,7 +171,7 @@
     1.4  \begin{descr}
     1.5  \item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
     1.6    follows.  The first occurrence of $\ALSO$ in some calculational thread
     1.7 -  initialises $calculation$ by $this$. Any subsequent $\ALSO$ on the same
     1.8 +  initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
     1.9    level of block-structure updates $calculation$ by some transitivity rule
    1.10    applied to $calculation$ and $this$ (in that order).  Transitivity rules are
    1.11    picked from the current context plus those given as $thms$ (the latter have
    1.12 @@ -252,7 +252,7 @@
    1.13  \end{matharray}
    1.14  
    1.15  \begin{rail}
    1.16 -  'simp' (simpmod * )
    1.17 +  'simp' ('!' ?) (simpmod * )
    1.18    ;
    1.19  
    1.20    simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
    1.21 @@ -264,21 +264,16 @@
    1.22    adding or deleting rules as specified.  The \railtoken{only} modifier first
    1.23    removes all other rewrite rules and congruences, and then is like
    1.24    \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
    1.25 -  nevertheless there may be side-effects on the context via attributes.  This
    1.26 -  provides a back door for arbitrary context manipulation.
    1.27 +  nevertheless there may be side-effects on the context via
    1.28 +  attributes.\footnote{This provides a back door for arbitrary context
    1.29 +    manipulation.}
    1.30    
    1.31 -  The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
    1.32 -  \cite[\S10]{isabelle-ref}), but is much better behaved in practice.  Only
    1.33 -  the local premises of the actual goal are involved by default.  Additional
    1.34 -  facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
    1.35 -  The full context of assumptions is
    1.36 -
    1.37 -; $simp$ removes any premises of the goal, before
    1.38 -  inserting the goal facts; $asm_simp$ leaves the premises.  Thus $asm_simp$
    1.39 -  may refer to premises that are not explicitly spelled out, potentially
    1.40 -  obscuring the reasoning.  The plain $simp$ method is more faithful in the
    1.41 -  sense that, apart from the rewrite rules of the current context, \emph{at
    1.42 -    most} the explicitly provided facts may participate in the simplification.
    1.43 +  The $simp$ method is based on \texttt{asm_full_simp_tac}
    1.44 +  \cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
    1.45 +  local premises of the actual goal are involved by default.  Additional facts
    1.46 +  may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
    1.47 +  full context of assumptions is only included in the $simp!$ version, which
    1.48 +  should be used with care.
    1.49  \end{descr}
    1.50  
    1.51  \subsection{Modifying the context}
    1.52 @@ -311,8 +306,11 @@
    1.53  \end{matharray}
    1.54  
    1.55  These attributes provide forward rules for simplification, which should be
    1.56 -used only very rarely.  See the ML functions of the same name in
    1.57 -\cite[\S10]{isabelle-ref} for more information.
    1.58 +used only very rarely.  There are no separate options for adding or deleting
    1.59 +simplification rules locally.
    1.60 +
    1.61 +See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
    1.62 +information.
    1.63  
    1.64  
    1.65  \section{The Classical Reasoner}
    1.66 @@ -334,19 +332,19 @@
    1.67  
    1.68  \begin{descr}
    1.69  \item [$rule$] as offered by the classical reasoner is a refinement over the
    1.70 -  primitive one (see \S\ref{sec:pure-meth}).  In the case that no rules are
    1.71 +  primitive one (see \S\ref{sec:pure-meth}).  In case that no rules are
    1.72    provided as arguments, it automatically determines elimination and
    1.73    introduction rules from the context (see also \S\ref{sec:classical-mod}).
    1.74    In that form it is the default method for basic proof steps, such as
    1.75    $\PROOFNAME$ and ``$\DDOT$'' (two dots).
    1.76    
    1.77  \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
    1.78 -  elim-resolution, after having inserted the facts.  Omitting the arguments
    1.79 +  elim-resolution, after having inserted any facts.  Omitting the arguments
    1.80    refers to any suitable rules from the context, otherwise only the explicitly
    1.81    given ones may be applied.  The latter form admits better control of what
    1.82    actually happens, thus it is very appropriate as an initial method for
    1.83    $\PROOFNAME$ that splits up certain connectives of the goal, before entering
    1.84 -  the sub-proof.
    1.85 +  the actual proof.
    1.86    
    1.87  \item [$contradiction$] solves some goal by contradiction, deriving any result
    1.88    from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
    1.89 @@ -370,9 +368,9 @@
    1.90  \railterm{slowbest}
    1.91  
    1.92  \begin{rail}
    1.93 -  'blast' nat? (clamod * )
    1.94 +  'blast' ('!' ?) nat? (clamod * )
    1.95    ;
    1.96 -  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
    1.97 +  ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
    1.98    ;
    1.99  
   1.100    clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
   1.101 @@ -401,7 +399,7 @@
   1.102  \end{matharray}
   1.103  
   1.104  \begin{rail}
   1.105 -  ('force' | 'auto') (clasimpmod * )
   1.106 +  ('force' | 'auto') ('!' ?) (clasimpmod * )
   1.107    ;
   1.108  
   1.109    clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
   1.110 @@ -413,8 +411,8 @@
   1.111    simplification and classical reasoning tactics.  See \texttt{force_tac} and
   1.112    \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   1.113    modifier arguments correspond to those given in \S\ref{sec:simp} and
   1.114 -  \S\ref{sec:classical-auto}.  Note that the ones related to the Simplifier
   1.115 -  are prefixed by \railtoken{simp} here.
   1.116 +  \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.117 +  Simplifier are prefixed by \railtoken{simp} here.
   1.118  \end{descr}
   1.119  
   1.120  \subsection{Modifying the context}\label{sec:classical-mod}
   1.121 @@ -448,7 +446,6 @@
   1.122    first, e.g.\ by using the $elimify$ attribute.
   1.123  \end{descr}
   1.124  
   1.125 -
   1.126  %%% Local Variables: 
   1.127  %%% mode: latex
   1.128  %%% TeX-master: "isar-ref"