Simplifier options;
authorwenzelm
Thu Apr 13 15:02:02 2000 +0200 (2000-04-13)
changeset 8704f76f41f24c44
parent 8703 816d8f6513be
child 8705 a3da5538d924
Simplifier options;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Apr 13 15:01:50 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Apr 13 15:02:02 2000 +0200
     1.3 @@ -379,10 +379,21 @@
     1.4  \railalias{simpall}{simp\_all}
     1.5  \railterm{simpall}
     1.6  
     1.7 +\railalias{noasm}{no\_asm}
     1.8 +\railterm{noasm}
     1.9 +
    1.10 +\railalias{noasmsimp}{no\_asm\_simp}
    1.11 +\railterm{noasmsimp}
    1.12 +
    1.13 +\railalias{noasmuse}{no\_asm\_use}
    1.14 +\railterm{noasmuse}
    1.15 +
    1.16  \begin{rail}
    1.17 -  ('simp' | simpall) ('!' ?) (simpmod * )
    1.18 +  ('simp' | simpall) ('!' ?) simpopt? (simpmod * )
    1.19    ;
    1.20  
    1.21 +  simpopt: (noasm | noasmsimp | noasmuse) ':'
    1.22 +  ;
    1.23    simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
    1.24    ;
    1.25  \end{rail}
    1.26 @@ -404,15 +415,28 @@
    1.27  \item [$simp_all$] is similar to $simp$, but acts on all goals.
    1.28  \end{descr}
    1.29  
    1.30 -Internally, the $simp$ method is based on \texttt{asm_full_simp_tac}
    1.31 -\cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
    1.32 -local premises of the actual goal are involved by default.  Additional facts
    1.33 -may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
    1.34 -full context of assumptions is only included in the $simp!$ version, which
    1.35 -should be used with some care, though.
    1.36 +By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
    1.37 +internally \cite[\S10]{isabelle-ref}.  In structured proofs this is usually
    1.38 +quite well behaved in practice: just the local premises of the actual goal are
    1.39 +involved, additional facts may inserted via explicit forward-chaining (using
    1.40 +$\THEN$, $\FROMNAME$ etc.).  The full context of assumptions is only included
    1.41 +if the ``$!$'' (bang) argument is given, which should be used with some care,
    1.42 +though.
    1.43  
    1.44 -Note that there is no separate $split$ method.  The effect of
    1.45 -\texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~\vec a)$.
    1.46 +Additional Simplifier options may be specified to tune the behavior even
    1.47 +further: $no_asm$ means assumptions are ignored completely (cf.\ 
    1.48 +\texttt{simp_tac}), $no_asm_simp$ means assumptions are used in the
    1.49 +simplification of the conclusion but are not themselves simplified (cf.\ 
    1.50 +\texttt{asm_simp_tac}), and $no_asm_use$ means assumptions are simplified but
    1.51 +are not used in the simplification of each other or the conclusion (cf.
    1.52 +\texttt{full_simp_tac}).
    1.53 +
    1.54 +\medskip
    1.55 +
    1.56 +The Splitter package is usually configured to work as part of the Simplifier.
    1.57 +There is no separate $split$ method available.  The effect of repeatedly
    1.58 +applying \texttt{split_tac} can be simulated by
    1.59 +$(simp~only\colon~split\colon~\vec a)$.
    1.60  
    1.61  
    1.62  \subsection{Declaring rules}