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?


isabelle-dev mailing list

Reply via email to