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

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.


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.