[isabelle-dev] simplifier trace (and jedit)
makarius at sketis.net
Wed May 23 15:24:52 CEST 2012
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)
> 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 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.
More information about the isabelle-dev