more on "Simplifier trace" (by Lars Hupel);
authorwenzelm
Mon Jul 21 15:16:50 2014 +0200 (2014-07-21)
changeset 5759006cb5375e189
parent 57589 e0e4ac981cf1
child 57591 8c095aef6769
more on "Simplifier trace" (by Lars Hupel);
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/document/root.tex
     1.1 --- a/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 14:24:10 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 15:16:50 2014 +0200
     1.3 @@ -893,6 +893,54 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 +subsection {* Simplifier trace \label{sec:simplifier-trace} *}
     1.8 +
     1.9 +text {*
    1.10 +  The new visual tracing facility is available in Isabelle/jEdit and
    1.11 +  provides a hierarchical representation of the rewriting steps
    1.12 +  performed by the simplifier.  It is intended to supersede the old
    1.13 +  textual tracing in a future release.
    1.14 +
    1.15 +  Users can configure the behaviour of the new tracing by specifying
    1.16 +  breakpoints, verbosity and enabling or disabling the interactive
    1.17 +  mode.  In normal verbosity (the default), only rule applications
    1.18 +  matching a breakpoint will be shown to the user.  In full verbosity,
    1.19 +  all rule applications will be logged.
    1.20 +
    1.21 +  There are two kinds of breakpoints: term and theorem breakpoints.
    1.22 +  Term breakpoints are patterns which are checked for matches on the
    1.23 +  redex of a rule application.  Theorem breakpoints trigger when the
    1.24 +  corresponding theorem is applied in a rewrite step.
    1.25 +
    1.26 +  In addition to that, the interactive mode interrupts the normal flow
    1.27 +  of the simplifier and defers the decision how to continue to the
    1.28 +  user.
    1.29 +
    1.30 +  \begin{matharray}{rcl}
    1.31 +    @{attribute simplifier_trace} & : & @{text attribute} \\
    1.32 +    @{attribute simp_break} & : & @{text attribute} \\
    1.33 +  \end{matharray}
    1.34 +
    1.35 +  @{rail \<open>
    1.36 +    @@{attribute simplifier_trace} ('interactive')? \<newline>
    1.37 +      ('mode' '=' ('full' | 'normal'))? \<newline>
    1.38 +      ('depth' '=' @{syntax nat})?
    1.39 +    ;
    1.40 +
    1.41 +    @@{attribute simp_break} (@{syntax term}*);
    1.42 +  \<close>}
    1.43 +
    1.44 +  The @{attribute simp_break} option can be used to declare both term
    1.45 +  and theorems, for example:
    1.46 +*}
    1.47 +
    1.48 +declare conjI[simp_break]
    1.49 +declare [[simp_break "?x \<and> ?y"]]
    1.50 +
    1.51 +text{*
    1.52 +  The other options behave in a similar way as for the old trace (see
    1.53 +  \secref{sec:simp-config}).
    1.54 +*}
    1.55  
    1.56  subsection {* Simplification procedures \label{sec:simproc} *}
    1.57  
     2.1 --- a/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 14:24:10 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 15:16:50 2014 +0200
     2.3 @@ -34,14 +34,15 @@
     2.4    Lucas Dixon,
     2.5    Florian Haftmann, \\
     2.6    Brian Huffman,
     2.7 -  Gerwin Klein,
     2.8 -  Alexander Krauss, \\
     2.9 +  Lars Hupel,
    2.10 +  Gerwin Klein, \\
    2.11 +  Alexander Krauss,
    2.12    Ond\v{r}ej Kun\v{c}ar,
    2.13 -  Andreas Lochbihler,
    2.14 -  Tobias Nipkow, \\
    2.15 +  Andreas Lochbihler, \\
    2.16 +  Tobias Nipkow,
    2.17    Lars Noschinski,
    2.18 -  David von Oheimb,
    2.19 -  Larry Paulson, \\
    2.20 +  David von Oheimb, \\
    2.21 +  Larry Paulson,
    2.22    Sebastian Skalberg,
    2.23    Christian Sternagel
    2.24  }