doc-src/IsarRef/generic.tex
changeset 9799 038b018f86f5
parent 9780 d25d6a977ea6
child 9847 32ce11c3f6b1
     1.1 --- a/doc-src/IsarRef/generic.tex	Sat Sep 02 21:46:04 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Sep 02 21:47:08 2000 +0200
     1.3 @@ -635,7 +635,7 @@
     1.4  \begin{rail}
     1.5    'subst' thmref
     1.6    ;
     1.7 -  'split' thmrefs
     1.8 +  'split' ('(' 'asm' ')')? thmrefs
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12 @@ -650,6 +650,9 @@
    1.13    which may be either a meta or object equality.
    1.14  \item [$hypsubst$] performs substitution using some assumption.
    1.15  \item [$split~thms$] performs single-step case splitting using rules $thms$.
    1.16 +  By default, splitting is performed in the conclusion of a goal; the $asm$
    1.17 +  option indicates to operate on assumptions instead.
    1.18 +  
    1.19    Note that the $simp$ method already involves repeated application of split
    1.20    rules as declared in the current context (see \S\ref{sec:simp}).
    1.21  \item [$symmetric$] applies the symmetry rule of meta or object equality.
    1.22 @@ -699,11 +702,12 @@
    1.23  
    1.24  \subsection{Automated methods}\label{sec:classical-auto}
    1.25  
    1.26 -\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}
    1.27 -\indexisarmeth{safe}\indexisarmeth{clarify}
    1.28 +\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
    1.29 +\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
    1.30  \begin{matharray}{rcl}
    1.31    blast & : & \isarmeth \\
    1.32    fast & : & \isarmeth \\
    1.33 +  slow & : & \isarmeth \\
    1.34    best & : & \isarmeth \\
    1.35    safe & : & \isarmeth \\
    1.36    clarify & : & \isarmeth \\
    1.37 @@ -712,7 +716,7 @@
    1.38  \begin{rail}
    1.39    'blast' ('!' ?) nat? (clamod * )
    1.40    ;
    1.41 -  ('fast' | 'best' | 'clarify' | 'safe') ('!' ?) (clamod * )
    1.42 +  ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod * )
    1.43    ;
    1.44  
    1.45    clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
    1.46 @@ -726,9 +730,10 @@
    1.47    classical proof procedure in Isabelle that can handle actual object-logic
    1.48    rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
    1.49    facts).
    1.50 -\item [$fast$, $best$, $safe$, and $clarify$] refer to the generic classical
    1.51 -  reasoner.  See \texttt{fast_tac}, \texttt{best_tac}, \texttt{safe_tac}, and
    1.52 -  \texttt{clarify_tac} in \cite[\S11]{isabelle-ref} for more information.
    1.53 +\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
    1.54 +  classical reasoner.  See \texttt{fast_tac}, \texttt{slow_tac},
    1.55 +  \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
    1.56 +  \cite[\S11]{isabelle-ref} for more information.
    1.57  \end{descr}
    1.58  
    1.59  Any of above methods support additional modifiers of the context of classical
    1.60 @@ -743,19 +748,21 @@
    1.61  
    1.62  \subsection{Combined automated methods}
    1.63  
    1.64 -\indexisarmeth{auto}\indexisarmeth{force}
    1.65 -\indexisarmeth{clarsimp}\indexisarmeth{fastsimp}
    1.66 +\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
    1.67 +\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
    1.68  \begin{matharray}{rcl}
    1.69    auto & : & \isarmeth \\
    1.70    force & : & \isarmeth \\
    1.71    clarsimp & : & \isarmeth \\
    1.72    fastsimp & : & \isarmeth \\
    1.73 +  slowsimp & : & \isarmeth \\
    1.74 +  bestsimp & : & \isarmeth \\
    1.75  \end{matharray}
    1.76  
    1.77  \begin{rail}
    1.78    'auto' '!'? (nat nat)? (clasimpmod * )
    1.79    ;
    1.80 -  ('force' | 'clarsimp' | 'fastsimp') '!'? (clasimpmod * )
    1.81 +  ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod * )
    1.82    ;
    1.83  
    1.84    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
    1.85 @@ -764,12 +771,12 @@
    1.86  \end{rail}
    1.87  
    1.88  \begin{descr}
    1.89 -\item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's
    1.90 -  combined simplification and classical reasoning tactics.  These correspond
    1.91 -  to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and
    1.92 -  \texttt{fast_tac} (with the Simplifier added as wrapper), see
    1.93 -  \cite[\S11]{isabelle-ref} for more information.  The modifier arguments
    1.94 -  correspond to those given in \S\ref{sec:simp} and
    1.95 +\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
    1.96 +  provide access to Isabelle's combined simplification and classical reasoning
    1.97 +  tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
    1.98 +  \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
    1.99 +  added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
   1.100 +  modifier arguments correspond to those given in \S\ref{sec:simp} and
   1.101    \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.102    Simplifier are prefixed by \railtterm{simp} here.
   1.103