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




Am 18/11/2012 10:51, schrieb Joachim Breitner:
> 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.
> 
> great!
> 
>>> 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?

We don't forbid that at all. We just don't want to encourage it in general.

> (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.)

Sledgehammer (currently) has no alternative.

Tobias

> Greetings, Joachim
> 





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