[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants
nschirmer at apple.com
Sat Oct 2 10:51:11 CEST 2021
> On 29. Sep 2021, at 12:19, Makarius <makarius at sketis.net> wrote:
> Are there any remaining uses of your alternative antiquotations that are not
> covered properly by the new official scheme?
In AutoCorres there are also alternative antiquotations for matching and building terms, similar to the ones presented by Peter:
Also I see great potential for providing similar antiquotations also for cterms, offering the possibility to ‘match’ sub-cterms and build cterms from certified sub-cterms. In contrast to terms also the matching part will result in a matching function, as cterms are an abstract data type.
In my experience recertifying cterms in proof tools like simprocs or tactics can easily become a performance hot-spot when terms become large.
As taking apart and recombining cterms manually with functions like Thm.dest_comb / Thm.apply is quite verbose and hard to maintain it rarely is used in practise. Instead terms are decomposed by ML-matching, recombined and recertified. In the presence of your new antiquotations this idiom is likely to become even more attractive and commonplace.
Having antiquotations for cterms can be a powerful show-case for the potential of antiquotations, bringing together readability / conciseness as well as scalability.
Norbert Schirmer (nschirmer at apple.com)
SEG Formal Verification
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev