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



Thanks for the suggestion, but this is getting a bit fine-grained and I can
imagine (too) many variations on this idea.

Tobias

Am 25/11/2012 23:26, schrieb Timothy Bourke:
> On Nov 18 at 09:31 +0100, Tobias Nipkow wrote:
>> Am 16/11/2012 23:25, schrieb Joachim Breitner:
>>> Is there a chance to get a similar feature for the simplifier? I could
>>>  imagine that when I write apply (simp minimize add: foo) the
>>> simplifier would run as usual, but it would also keep track of which
>>> simplification rules were actually used.
>> 
>> 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 wonder if such a feature would be more practical and useful if restricted
> to a particular theory (or set of theories):
> 
> apply (simp minimize: Invariants add: foo)
> 
> where rules from a theory called "Invariants" would be listed for possible
> one-click substitution.
> 
> During the verification of a model, for instance, it's certainly more 
> efficient (for the user) to have most lemmas applied automatically, but
> afterward it would sometimes be nice to know exactly which lemmas (from a
> subset of interesting ones) were actually used. Both for refactoring, as
> already mentioned, and for better understanding the result.
> 
> But, perhaps this would be better in a separate "reporting tool"?
> 
> Tim.
> 





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