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.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
