Re: [isabelle] Feature wish: Minimal simp/auto invocations

Dear Tobias,

Am Sonntag, den 18.11.2012, 09:31 +0100 schrieb Tobias Nipkow:
> We are planning to provide a much improved tracing facility for the simplifier
> which will certainly keep track of such things and will tell you, for example,
> if a rule you added explicitly was not used at all. We could also provide the
> list of all rules used.


> > The output window would then say something along the lines simplification
> > used 5 lemmas. Use "apply (simp only: foo bar baz bam bang)" (12ms) to 
> > reproduce. and in the IDE I could click on that to replace the original
> > invocation with this more explicit command.
> I doubt we want to go down that route. The simplifier often uses lots of
> rules, which would lead to a very long list if supplied explicitly, which is
> ugly. Moreover it would expose information we want to hide: how exactly a lot
> of basic computations are organized, especially rewriting on numbers. Your
> suggestion would create simplifier calls that hardwire that information and
> make such steps very brittle under change. I don't want to encourage that.

I understand the rationale here, and it certainly makes sense when
working with a theory that does, say, lots of arithmetic. But other
applications may make very little use of basic stuff from Main; hardly
more than just lists. I’d suggest that the call should be left to the
user: If he sees lots of lemmas he did not write himself or does not
know, he can leave the simp call as it is. But if the lemmas are roughly
what he expected, why not allow him to make that explicit?

(The situation is not different with sledgehammer, which also
occasionally produces internal lemmas, yet it is a useful feature that
is mostly used in a “good” way.)


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.