On Wed, 23 May 2012, Christian Sternagel wrote:

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)?

The printed name is of a different category, which is vaguely related to the internal derivation object (PThm), but not exactly that. These names should hardly ever occur to the user, but there are some historical left-overs as seen here.

The Prover IDE markup already provides a good deal of authentic source position information, so one could extend this to cover thm values as well. For example, when I see `prop` in the text, I often want to C-click on it to get to the place where the corresponding fact was introduced, but the tiny goal/tactic derivation gets between the result and its origin in the source.

The simplifier has similar adhoc derivations in mksimps. Another problem are morphisms applied before addsimps. This distance to the source somehow needs to be formalized in a more robust manner.

isabelle-dev mailing list

Reply via email to