[isabelle-dev] simplifier trace (and jedit)

[Makarius]

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