Thanks a lot for the explanations and examples and work into the direction to improve performance in the mid-term.
I guess with some combination of hand-crafted declarations (instead of attributes) and implementing the ‘def’ idea above I can improve the performance for our applications.
The tradeoff is between simplicity / readability vs. performance. Especially the neat thing about attributes (compared to declarations) is that you can already provide them to almost all relevant functions like definitions, derived specifications (like function package) and ’notes’. Note that we not only use plain definitions with large terms but also derived concepts like (partial) functions which besides the defining equation also result in a bunch of theorems (like induction) with large terms.
My main working-horse is actually the ’named_theorems’ attribute which is only relevant in the body of the locale when doing proofs and not in the declaration of new locales. So I would reimplement this functionality with a declaration instead of the existing attribute, explicitly postponing the application of the morphism. Thats why I mentioned the idea of “lazy attributes” to implement an attribute like “lazy_named_theorems” that can be provided to all the already existing functions in Isabelle/ML.
Norbert Schirmer (nschirmer at apple.com)
SEG Formal Verification