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

That is a version of the feedback we intend to give: which of the added rules
were actually used.


Am 18/11/2012 13:10, schrieb Manuel Eberl:
> What i would find more useful would be output in the form of 'Use "apply
> (simp add: foo bar baz bam bang)"', i. e. if it showed a list of the
> rewrite rules that it used and that are not in the simp set anyway.
> This, if I am not mistaken, would not lead to the problem of exposing
> any of these these internal details but still provide a similar
> functionality. I for one use "simp add:" much more often than "simp
> only:" and have often found myself removing rules from the "add" clause
> by trial and error to find out which of them are actually necessary.
> Cheers,
> Manuel
> On 18/11/12 09:31, Tobias Nipkow wrote:
>>> 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.

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