[isabelle-dev] simplifier trace (and jedit)

[Thomas Sewell]

The _2 v.s. (2) thing is just silly. It's in find_theorems output too. 
It's just the way theorems get their names - probably one of these 
decisions made years ago and not compatible with Makarius' decisions 
about how to fetch theorems in Isar.

Adding context information to every reduction sounds too big in most 
cases - both for human consumption and for processing by fragile 
processes like ProofGeneral. I agree with you though that context can be 
hard to follow.

As for (simp only: ) vs unfolding - your rule is of the form "Not (Suc 
nat = 0)" which the simplifier preprocesses into "(Suc nat = 0) == 
False" but which the naive unfolder processes as "(Not (Suc nat = 0)) == 
True". That is, without further setup, the rule is not really an 
unfoldable rule.

Yours,
     Thomas.

On 23/05/12 14:15, Christian Sternagel wrote:
> Dear all,
>
> I wanted to write this already a long time ago (prompted by an Isabelle
> course I gave) but somehow forgot about it. Now I had a look at my
> slides again and was reminded.
>
> 1) The first thing is rather subjective, but maybe you could comment on
> it. I think the simplifier trace would be less surprising for newbies
> and slightly easier to read if
> - names of rewrite rules would be printed in their original form.
> Consider, e.g., the trace resulting from
>
>     lemma "Suc 0 + 0 = 0"
>       using [[simp_trace]]
>       apply simp
>
> where we have (among others)
>
>     [1]Applying instance of rewrite rule "Nat.nat.distinct_2":
>     Suc ?nat'2 = 0 ≡ False
>
> Why not use the "real" name "Nat.nat.distinct(2)" in the trace (Okay,
> the rule was "preprocessed" by the simplifier, but still, as far as I
> can tell the printed name does not exist)?
>
> - in the "[1]Rewriting:" messages, we actually just see the redex and
> the contractum, but not the context of a rewrite step. Why not show the
> whole terms? (One reason against this is the high redundancy and
> potentially huge size of such traces, but on the other hand, they are
> traces and only generated when requested.)
>
> 2) Some questions concerning the trace:
> - When I explicitly use a single rule by "unfolding rule-name", why is
> there more in the trace than just the application of this rule?
>
> - Why does "apply (simp only: rule)" and "unfolding rule" behave
> differently? E.g., on the term "Suc 0 = 0" with rule
> "Nat.nat.distinct(2)" the former results in "False", whereas the latter
> does nothing. Is it important that those two commands behave differently?
>
> 3) Furthermore, in my course I recommend students (which know about term
> rewriting before) to have a look at the simplifier trace whenever the
> simplifier does something unexpected or does not terminate. However, for
> the latter use-case (i.e., finding cause of nontermination) I do not
> even know how to do it myself in jedit. As soon as I write, e.g., "apply
> simp" the simplifier starts to loop, if I don't delete the command it
> continues looping (and thus the whole system becomes highly unresponsive
> very soon), if I delete the command, the trace is gone too. Is there any
> way (or workaround), such that I can generate (part of) the trace of a
> (potentially) looping reduction. Maybe giving a timeout to "apply simp"
> (but I don't know whether or how this is possible) does work?
>
> cheers
>
> chris
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev