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.


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?


isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to