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



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.

Attachment: signature.asc
Description: Digital signature



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