[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

[Norbert Schirmer]

> 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:
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy>


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.



Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211002/6080b9b1/attachment.htm>