[isabelle-dev] simplifier trace (and jedit)

[Christian Sternagel]

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